-- 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.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 (⇑g ∘ f) s) s x) (m 0)) (tail m) =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Tactic:
simp_rw [Z]

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 𝕜 (⇑(compContinuousMultilinearMapL (fun x => E) g) ∘ iteratedFDerivWithin 𝕜 i f s) s x) (m 0))
      (tail 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
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s) s x) (m 0)) (tail m) =
    ((↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 (i + 1) f s x)) m

Tactic:
have Z : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (g ∘ f) s) s x =
    fderivWithin 𝕜 (g.compContinuousMultilinearMapL (fun _ : Fin i => E) ∘
      iteratedFDerivWithin 𝕜 i f s) s x :=
  fderivWithin_congr' (@IH) 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
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s) s x) (m 0)) (tail 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
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s x) (m 0)) (tail m) = (iteratedFDerivWithin 𝕜 (i + 1) f s x) m

Tactic:
rw [iteratedFDerivWithin_succ_apply_left]

Result:
no goals

Proof state:
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

Tactic:
simp only [iteratedFDerivWithin_zero_apply, comp_apply,
  ContinuousLinearMap.compContinuousMultilinearMap_coe, coe_coe]

Result:
no goals

Proof state:
𝕜 : 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
x : E
g : F ≃L[𝕜] G
f : E → F
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
i : ℕ
⊢ iteratedFDerivWithin 𝕜 i (⇑g ∘ f) s x = (↑g).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
induction' i with i IH generalizing x

Result:
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)

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)