Theorem: fderiv_iteratedFDeriv_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
m : Fin n → F
x v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ ↑n < ↑(Nat.succ n)
Tactic:
norm_cast
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
m : Fin n → F
x v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ n < Nat.succ n

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
m : Fin n → F
x v : F
hf : ContDiff 𝕜 (↑(Nat.succ n)) f
⊢ n < Nat.succ n
Tactic:
simp
State after:
no goals