C^∞_loc convergence is preserved under composition

import Definitions.Def_FiniteEnergyPlane_Setting

namespace FiniteEnergyPlane

open MeasureTheory Metric Filter Topology
open scoped ContDiff ENNReal Real

/-- `C^∞_loc` convergence is preserved under composition. Let `U ⊆ X` and `W ⊆ Y` be open, with
`Y` finite-dimensional. Let `f_k, f : U → W` be smooth with `f_k → f` in `C^∞_loc(U)`, and let
`g_k, g` be smooth on `W` with `g_k → g` in `C^∞_loc(W)`. Then `g_k ∘ f_k → g ∘ f` in
`C^∞_loc(U)`. -/
theorem tendstoCInftyLocOn_comp {X Y Z : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [FiniteDimensional ℝ Y] [NormedAddCommGroup Z]
    [NormedSpace ℝ Z] {U : Set X} (hU : IsOpen U) {W : Set Y} (hW : IsOpen W)
    (f : ℕ → X → Y) (f₀ : X → Y) (g : ℕ → Y → Z) (g₀ : Y → Z)
    (hf : ∀ k, ContDiffOn ℝ ∞ (f k) U) (hf₀ : ContDiffOn ℝ ∞ f₀ U)
    (hg : ∀ k, ContDiffOn ℝ ∞ (g k) W) (hg₀ : ContDiffOn ℝ ∞ g₀ W)
    (hfW : ∀ k, Set.MapsTo (f k) U W) (hf₀W : Set.MapsTo f₀ U W)
    (hff : JHolomorphic.TendstoCInftyLocOn f f₀ U) (hgg : JHolomorphic.TendstoCInftyLocOn g g₀ W) :
    JHolomorphic.TendstoCInftyLocOn (fun k => g k ∘ f k) (g₀ ∘ f₀) U := by
  sorry

end FiniteEnergyPlane