-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_left (g : F ≃L[𝕜] G) (f : E → F)
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (i : ℕ) :
    iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
      (g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)

Proof state:
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 (i + 1) (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)

Tactic:
ext1 m

Result:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (⇑g ∘ f) s x) m =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Proof state:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
Z :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s) s x =
    fderivWithin 𝕜 (⇑(compContinuousMultilinearMapL (fun x => E) g) ∘ iteratedFDerivWithin 𝕜 i f s) s x
⊢ (((↑(compContinuousMultilinearMapL (fun x => E) g)).comp (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x)) (m 0))
      (tail m) =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Tactic:
simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
  ContinuousLinearEquiv.compContinuousMultilinearMapL_apply,
  ContinuousLinearMap.compContinuousMultilinearMap_coe, EmbeddingLike.apply_eq_iff_eq]

Result:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
Z :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s) s x =
    fderivWithin 𝕜 (⇑(compContinuousMultilinearMapL (fun x => E) g) ∘ iteratedFDerivWithin 𝕜 i f s) s x
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (m 0)) (tail m) = (iteratedFDerivWithin 𝕜 (i + 1) f s x) m

Proof state:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
Z :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s) s x =
    fderivWithin 𝕜 (⇑(compContinuousMultilinearMapL (fun x => E) g) ∘ iteratedFDerivWithin 𝕜 i f s) s x
⊢ ((fderivWithin 𝕜 (⇑(compContinuousMultilinearMapL (fun x => E) g) ∘ iteratedFDerivWithin 𝕜 i f s) s x) (m 0))
      (tail m) =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Tactic:
rw [(g.compContinuousMultilinearMapL fun _ : Fin i => E).comp_fderivWithin (hs x hx)]

Result:
case succ.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : E},
    x ∈ s → iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
Z :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s) s x =
    fderivWithin 𝕜 (⇑(compContinuousMultilinearMapL (fun x => E) g) ∘ iteratedFDerivWithin 𝕜 i f s) s x
⊢ (((↑(compContinuousMultilinearMapL (fun x => E) g)).comp (fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x)) (m 0))
      (tail m) =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Proof state:
case zero
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 0 (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 0 f s x)

Tactic:
ext1 m

Result:
case zero.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
m : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (⇑g ∘ f) s x) m = ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 0 f s x)) m