-- Module: Mathlib.Analysis.Calculus.ContDiff.Basic
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
x : E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
zero :
  ∀ {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin 0) ↦ E) G)
      (iteratedFDerivWithin 𝕜 0 ((⇑g : (a : F) → G) ∘ f) s x)
      ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ E) (iteratedFDerivWithin 𝕜 0 f s x))
zero₁ :
  ∀ {x : E} (hx : x ∈ s) (m : (i : Fin 0) → E),
    Eq.{u_4 + 1} (α := G) ((iteratedFDerivWithin 𝕜 0 ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin 0) → E) → G) m : G)
      (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin 0) ↦ E) (iteratedFDerivWithin 𝕜 0 f s x) :
            (a : (i : Fin 0) → E) → G)
          m :
        G)
succ :
  ∀ (i : ℕ)
    (IH :
      ∀ {x : E} (hx : x ∈ s),
        Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
          (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
          ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)))
    {x : E} (hx : x ∈ s),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin (i + 1)) ↦ E) G)
      (iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x)
      ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
        (iteratedFDerivWithin 𝕜 (i + 1) f s x))
succ₁ :
  ∀ (i : ℕ)
    (IH :
      ∀ {x : E} (hx : x ∈ s),
        Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
          (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
          ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x)))
    {x : E} (hx : x ∈ s) (m : (i : Fin (i + 1)) → E),
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 (i + 1) ((⇑g : (a : F) → G) ∘ f) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
      (((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin (i + 1)) ↦ E)
              (iteratedFDerivWithin 𝕜 (i + 1) f s x) :
            (a : (i : Fin (i + 1)) → E) → G)
          m :
        G)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i ((⇑g : (a : F) → G) ∘ f) s x)
    ((↑g : F →L[𝕜] G).compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E) (iteratedFDerivWithin 𝕜 i f s x))

Tactic:
induction i generalizing x with ext1 m
  | zero =>
    simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, coe_coe]
  | succ i IH =>
    rw [iteratedFDerivWithin_succ_apply_left]
    have Z : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (g ∘ f) s) s x =
        fderivWithin 𝕜 (g.continuousMultilinearMapCongrRight (fun _ : Fin i => E) ∘
          iteratedFDerivWithin 𝕜 i f s) s x :=
      fderivWithin_congr' (@IH) hx
    simp_rw [Z]
    rw [(g.continuousMultilinearMapCongrRight fun _ : Fin i => E).comp_fderivWithin (hs x hx)]
    simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
      ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply,
      ContinuousLinearMap.compContinuousMultilinearMap_coe, EmbeddingLike.apply_eq_iff_eq]
    rw [iteratedFDerivWithin_succ_apply_left]

Premises used: ContinuousLinearMap.coe_comp', Fin.succ, EmbeddingLike.apply_eq_iff_eq, iteratedFDerivWithin_succ_apply_left, ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply, ContinuousLinearEquiv.continuousMultilinearMapCongrRight_apply, ContinuousLinearEquiv.comp_fderivWithin, ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_zero_apply, ContinuousLinearEquiv.continuousMultilinearMapCongrRight