Theorem: iteratedFDeriv_fderiv_apply_comm (ForML/ContinuousMultilinearMap.lean)

State before:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
x : F
m : Fin n → F
v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ (iteratedFDeriv 𝕜 n (fun y => (fderiv 𝕜 f y) v) x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) m) v
Tactic:
rw [contDiff_succ_iff_fderiv] at hf
State after:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
x : F
m : Fin n → F
v : F
hf : Differentiable 𝕜 f ∧ ContDiff 𝕜 ↑n fun y => fderiv 𝕜 f y
⊢ (iteratedFDeriv 𝕜 n (fun y => (fderiv 𝕜 f y) v) x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) m) v

State before:
ι : Type u_1
inst✝¹¹ : Fintype ι
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_4
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)
F : Type u_5
G : Type u_6
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
α : Type u_7
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace 𝕜 α
n : ℕ
f : F → G
x : F
m : Fin n → F
v : F
hf : Differentiable 𝕜 f ∧ ContDiff 𝕜 ↑n fun y => fderiv 𝕜 f y
⊢ (iteratedFDeriv 𝕜 n (fun y => (fderiv 𝕜 f y) v) x) m = ((iteratedFDeriv 𝕜 n (fun y => fderiv 𝕜 f y) x) m) v
Tactic:
rw [iteratedFDeriv_clm_apply_const_apply hf.right (le_refl _)]
State after:
no goals