-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_right (g : G ≃L[𝕜] E) (f : E → F)
    (hs : UniqueDiffOn 𝕜 s) {x : G} (hx : g x ∈ s) (i : ℕ) :
    iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
      (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g

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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x) (m 0)) (tail m) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i => g (m i))

Tactic:
have : fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
    fderivWithin 𝕜
      (ContinuousMultilinearMap.compContinuousLinearMapEquivL _ (fun _x : Fin i => g) ∘
        (iteratedFDerivWithin 𝕜 i f s ∘ g)) (g ⁻¹' 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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
this :
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x =
    fderivWithin 𝕜
      (⇑(ContinuousMultilinearMap.compContinuousLinearMapEquivL F fun _x => g) ∘ iteratedFDerivWithin 𝕜 i f s ∘ ⇑g)
      (⇑g ⁻¹' s) x
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x) (m 0)) (tail m) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i => g (m i))

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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
x : G
hx : g x ∈ s
x✝ : Fin 0 → G
⊢ (iteratedFDerivWithin 𝕜 0 (f ∘ ⇑g) (⇑g ⁻¹' s) x) x✝ =
    ((iteratedFDerivWithin 𝕜 0 f s (g x)).compContinuousLinearMap fun x => ↑g) x✝

Tactic:
simp only [iteratedFDerivWithin_zero_apply, comp_apply,
 ContinuousMultilinearMap.compContinuousLinearMap_apply]

Result:
no goals

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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
⊢ iteratedFDerivWithin 𝕜 (i + 1) (f ∘ ⇑g) (⇑g ⁻¹' s) x =
    (iteratedFDerivWithin 𝕜 (i + 1) f s (g x)).compContinuousLinearMap fun x => ↑g

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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (f ∘ ⇑g) (⇑g ⁻¹' s) x) m =
    ((iteratedFDerivWithin 𝕜 (i + 1) f s (g x)).compContinuousLinearMap fun x => ↑g) 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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (f ∘ ⇑g) (⇑g ⁻¹' s) x) m =
    ((iteratedFDerivWithin 𝕜 (i + 1) f s (g x)).compContinuousLinearMap fun x => ↑g) m

Tactic:
simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply,
  ContinuousLinearEquiv.coe_coe, iteratedFDerivWithin_succ_apply_left]

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 : G ≃L[𝕜] E
f : E → F
hs : UniqueDiffOn 𝕜 s
i : ℕ
IH :
  ∀ {x : G},
    g x ∈ s →
      iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s) x =
        (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun x => ↑g
x : G
hx : g x ∈ s
m : Fin (i + 1) → G
⊢ ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) (⇑g ⁻¹' s)) (⇑g ⁻¹' s) x) (m 0)) (tail m) =
    ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i f s) s (g x)) (g (m 0))) (tail fun i => g (m i))