-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem iteratedPDeriv_eq_iteratedFDeriv {n : ℕ} {m : Fin n → E} {f : 𝓢(E, F)} {x : E} :
    iteratedPDeriv 𝕜 m f x = iteratedFDeriv ℝ n f x m

Proof state:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ ((pderivCLM 𝕜 (m 0)) ((iteratedPDeriv 𝕜 (Fin.tail m)) f)) x =
    ((fderiv ℝ (iteratedFDeriv ℝ n ⇑f) x) (m 0)) (Fin.tail m)

Tactic:
rw [← fderiv_continuousMultilinear_apply_const_apply]

Result:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ ((pderivCLM 𝕜 (m 0)) ((iteratedPDeriv 𝕜 (Fin.tail m)) f)) x =
    (fderiv ℝ (fun y => (iteratedFDeriv ℝ n (⇑f) y) (Fin.tail m)) x) (m 0)

case succ.hc
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ DifferentiableAt ℝ (iteratedFDeriv ℝ n ⇑f) x

Proof state:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ ((pderivCLM 𝕜 (m 0)) ((iteratedPDeriv 𝕜 (Fin.tail m)) f)) x =
    (fderiv ℝ (fun y => (iteratedFDeriv ℝ n (⇑f) y) (Fin.tail m)) x) (m 0)

Tactic:
simp [← ih]

Result:
no goals

Proof state:
case succ.hc
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ DifferentiableAt ℝ (iteratedFDeriv ℝ n ⇑f) x

Tactic:
exact f.smooth'.differentiable_iteratedFDeriv (mod_cast ENat.coe_lt_top n) x

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
m : Fin 0 → E
x : E
⊢ ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ 0 (⇑f) x) m

Tactic:
simp

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ (n + 1) (⇑f) x) m

Tactic:
simp only [iteratedPDeriv_succ_left, iteratedFDeriv_succ_apply_left]

Result:
case succ
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : RCLike 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
ih : ∀ {m : Fin n → E} {x : E}, ((iteratedPDeriv 𝕜 m) f) x = (iteratedFDeriv ℝ n (⇑f) x) m
m : Fin (n + 1) → E
x : E
⊢ ((pderivCLM 𝕜 (m 0)) ((iteratedPDeriv 𝕜 (Fin.tail m)) f)) x =
    ((fderiv ℝ (iteratedFDeriv ℝ n ⇑f) x) (m 0)) (Fin.tail m)