-- 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
g : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)
i : ℕ
zero :
  ∀ {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 0) ↦ G) F)
      (iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
        (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E))
zero₁ :
  ∀ {x : G} (hx : Membership.mem (α := E) s ((g : (a : G) → E) x : E)) (m : (i : Fin 0) → G),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 0 (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x : (a : (i : Fin 0) → G) → F) m :
        F)
      ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin 0) ↦ G) (M₁' := fun (i : Fin 0) ↦ E)
              (iteratedFDerivWithin 𝕜 0 f s ((g : (a : G) → E) x)) fun (x : Fin 0) ↦ (↑g : G →L[𝕜] E) :
            (a : (i : Fin 0) → G) → F)
          m :
        F)
succ :
  ∀ (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)),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_4, u_3} 𝕜 (fun (i : Fin (i + 1)) ↦ G) F)
      (iteratedFDerivWithin 𝕜 (i + 1) (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x)
      (ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin (i + 1)) ↦ G) (M₁' :=
        fun (i : Fin (i + 1)) ↦ E) (iteratedFDerivWithin 𝕜 (i + 1) f s ((g : (a : G) → E) x)) fun (x : Fin (i + 1)) ↦
        (↑g : G →L[𝕜] E))
succ₁ :
  ∀ (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),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 (i + 1) (f ∘ (⇑g : (a : G) → E)) ((⇑g : (a : G) → E) ⁻¹' s) x :
            (a : (i : Fin (i + 1)) → G) → F)
          m :
        F)
      ((ContinuousMultilinearMap.compContinuousLinearMap (M₁ := fun (i : Fin (i + 1)) ↦ G) (M₁' :=
              fun (i : Fin (i + 1)) ↦ E) (iteratedFDerivWithin 𝕜 (i + 1) f s ((g : (a : G) → E) x))
              fun (x : Fin (i + 1)) ↦ (↑g : G →L[𝕜] E) :
            (a : (i : Fin (i + 1)) → G) → F)
          m :
        F)
⊢ 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))

Tactic:
induction i generalizing x with ext1 m
  | zero =>
    simp only [iteratedFDerivWithin_zero_apply, comp_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
  | succ i IH =>
    simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
      ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_succ_apply_left]
    have : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
        fderivWithin 𝕜
          (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft _ (fun _x : Fin i => g) ∘
            (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' s) x :=
      fderivWithin_congr' (@IH) hx
    rw [this, ContinuousLinearEquiv.comp_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]
    simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
      ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply,
      ContinuousMultilinearMap.compContinuousLinearMap_apply]
    rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
      ContinuousLinearMap.coe_comp', coe_coe, comp_apply, tail_def, tail_def]

Premises used: Iff.mpr, ContinuousLinearMap.coe_comp', Fin.succ, iteratedFDerivWithin_succ_apply_left, ContinuousLinearEquiv.comp_right_fderivWithin, ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply, ContinuousLinearEquiv.uniqueDiffOn_preimage_iff, Function.comp_apply, Fin.tail_def, ContinuousLinearEquiv.comp_fderivWithin, ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_zero_apply