-- 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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
      (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin i) ↦ G) (M₁' := fun (i : Fin i) ↦ E)
        (iteratedFDerivWithin 𝕜 i f s ((g : (a : G) → E) x)) fun (x : Fin i) ↦ (↑g : G →L[𝕜] E))
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
m : (i : Fin (i + 1)) → G
this :
  Eq (α := G →L[𝕜] ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin i) ↦ G) F)
    (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s))
      ((⇑g : (a : G) → E) ⁻¹' s) x)
    (fderivWithin 𝕜
      (comp (β := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (_x : Fin i) ↦ E) F)
        (⇑(continuousMultilinearMapCongrLeft (E := fun (_x : Fin i) ↦ G) (E₁ := fun (_x : Fin i) ↦ E) F
              fun (_x : Fin i) ↦ g) :
          (a : ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F) →
            ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ G) F)
        (iteratedFDerivWithin 𝕜 i f s ∘ (⇑g : (a : G) → E)))
      ((⇑g : (a : G) → E) ⁻¹' s) x)
succ :
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) ∘SL (↑g : G →L[𝕜] E) :
                (a : G) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (_x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        fun (i_1 : Fin i) ↦ (g : (a : G) → E) (tail (α := fun (i : Fin (i + 1)) ↦ G) m i_1) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
      F)
succ₁ :
  Eq.{u_3 + 1} (α := F)
    ((comp (β := E)
            (⇑(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x)) :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F)
            (⇑(↑g : G →L[𝕜] E) : (a : G) → E) (m 0) :
          (a : (i : Fin i) → E) → F)
        fun (i_1 : Fin i) ↦ (g : (a : G) → E) (tail (α := fun (i : Fin (i + 1)) ↦ G) m i_1) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
      F)
succ₂ :
  Eq.{u_3 + 1} (α := F)
    ((comp (β := E)
            (⇑(fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x)) :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F)
            (⇑g : (a : G) → E) (m 0) :
          (a : (i : Fin i) → E) → F)
        fun (i_1 : Fin i) ↦ (g : (a : G) → E) (tail (α := fun (i : Fin (i + 1)) ↦ G) m i_1) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
      F)
succ₃ :
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (_x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        fun (i_1 : Fin i) ↦ (g : (a : G) → E) (tail (α := fun (i : Fin (i + 1)) ↦ G) m i_1) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
      F)
succ₄ :
  Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (_x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        fun (i_1 : Fin i) ↦ (g : (a : G) → E) ((fun (k : Fin i) ↦ m k.succ) i_1) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
      F)
⊢ Eq.{u_3 + 1} (α := F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x :
                (a : G) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (_x : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        fun (i_1 : Fin i) ↦ (g : (a : G) → E) (tail (α := fun (i : Fin (i + 1)) ↦ G) m i_1) :
      F)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
              ((g : (a : G) → E) (m 0)) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
          (a : (i : Fin i) → E) → F)
        (tail (α := fun (i : Fin (i + 1)) ↦ E) fun (i : Fin (i + 1)) ↦ (g : (a : G) → E) (m i) : (i : Fin i) → E) :
      F)
have succ₅ : Eq.{u_3 + 1} (α := F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (_x : Fin i) ↦ E) F)
            ((g : (a : G) → E) (m 0)) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (_x : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      fun (i_1 : Fin i) ↦ (g : (a : G) → E) ((fun (k : Fin i) ↦ m k.succ) i_1) :
    F)
  ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s ((g : (a : G) → E) x) :
              (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F)
            ((g : (a : G) → E) (m 0)) :
          ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin i) ↦ E) F) :
        (a : (i : Fin i) → E) → F)
      fun (k : Fin i) ↦ (g : (a : G) → E) (m k.succ) :
    F)
Tactic: rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
      ContinuousLinearMap.coe_comp', coe_coe, comp_apply, tail_def, tail_def]