-- Lean 4 proof step from Mathlib.Analysis.Calculus.ContDiff.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
f : E → F
n : ℕ∞ω
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →ᴬ[𝕜] E
A : (m : ℕ) →
  ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F →
    ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F :=
  fun (m : ℕ) (h : ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin m) ↦ E) F) ↦
    h.compContinuousLinearMap (M₁ := fun (i : Fin m) ↦ G) (M₁' := fun (i : Fin m) ↦ E) fun (x : Fin m) ↦ g.contLinear
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : (↑m : ℕ∞ω) < n
x : G
hx : Membership.mem (γ := Set G) ((⇑g : (a : G) → E) ⁻¹' s) x
e_8 :
  Eq (α := AddCommGroup (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instAddCommGroup (M₁ := fun (i : Fin m) ↦ G)) NormedAddCommGroup.toAddCommGroup
e_9 :
  HEq (α := Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instModule (M₁ := fun (i : Fin m) ↦ G)) (β :=
    Module 𝕜 (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)) NormedSpace.toModule
e_10 :
  Eq (α := TopologicalSpace (ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F))
    (ContinuousMultilinearMap.instTopologicalSpace (E := fun (i : Fin m) ↦ G)) UniformSpace.toTopologicalSpace
⊢ Eq (α := G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
    (ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ G)
        (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin m.succ) ↦ G) (M₁' :=
          fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) fun (x : Fin m.succ) ↦ g.contLinear) :
      G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
    (IsBoundedLinearMap.toContinuousLinearMap (A m) ⋯ ∘SL
        ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) ∘SL
          g.contLinear :
      G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F)
have h : ∀ (y : G) (v : (i : Fin m) → G),
  Eq.{u_3 + 1} (α := F)
    (((((ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ G)
                    (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin m.succ) ↦ G) (M₁' :=
                      fun (i : Fin m.succ) ↦ E) (p ((g : (a : G) → E) x) m.succ) fun (x : Fin m.succ) ↦ g.contLinear) :
                  G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F) :
                (a : G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ G) F)
              y :
            ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F) :
          (a : (i : Fin m) → G) → F)
        v :
      F)
    ((((IsBoundedLinearMap.toContinuousLinearMap (A m) sorry ∘SL
                  ContinuousMultilinearMap.curryLeft (Ei := fun (i : Fin m.succ) ↦ E)
                      (p ((g : (a : G) → E) x) m.succ) ∘SL
                    g.contLinear :
                (a : G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ G) F)
              y :
            ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin m) ↦ G) F) :
          (a : (i : Fin m) → G) → F)
        v :
      F)
Tactic: ext y v