-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem iteratedFDerivWithin_clm_apply_const_apply
    {s : Set E} (hs : UniqueDiffOn 𝕜 s) {c : E → F →L[𝕜] G}
    (hc : ContDiffOn 𝕜 n c s) {i : ℕ} (hi : i ≤ n) {x : E} (hx : x ∈ s) {u : F} {m : Fin i → E} :
    (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s x) m = (iteratedFDerivWithin 𝕜 i c s x) m u

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
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (((iteratedFDerivWithin 𝕜 i c s x) (tail m)).comp 0 +
        (fderivWithin 𝕜 (fun y => (iteratedFDerivWithin 𝕜 i c s y) (tail m)) s x).flip u)
      (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (tail m)) u

Tactic:
simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.comp_zero, zero_add]

Result:
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
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ ((fderivWithin 𝕜 (fun y => (iteratedFDerivWithin 𝕜 i c s y) (tail m)) s x) (m 0)) u =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (tail m)) u

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
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 (i + 1) c s x) m) u

Tactic:
have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
  hc.differentiableOn_iteratedFDerivWithin hi hs

Result:
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
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (iteratedFDerivWithin 𝕜 (i + 1) (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 (i + 1) c s x) m) u

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
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (fderivWithin 𝕜 (fun y => (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s y) (tail m)) s x) (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (tail m)) u

Tactic:
rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]

Result:
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
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ↑i ≤ n →
    ∀ {x : E},
      x ∈ s →
        ∀ {m : Fin i → E}, (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : ↑i < n
h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s) s
h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s
⊢ (fderivWithin 𝕜 (fun x => ((iteratedFDerivWithin 𝕜 i c s x) (tail m)) u) s x) (m 0) =
    (((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x) (m 0)) (tail m)) u

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
n : WithTop ℕ∞
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
hi : ↑0 ≤ n
x : E
hx : x ∈ s
m : Fin 0 → E
⊢ (iteratedFDerivWithin 𝕜 0 (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 0 c s x) m) u

Tactic:
simp

Result:
no goals