rw [iteratedFDeriv_const_of_ne hb]
case h₀
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : F →L[𝕜] G
u : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
b : ℕ
a✝ : b ∈ Finset.range (n + 1)
hb : b ≠ 0
⊢ ↑(Nat.choose n b) * ‖iteratedFDeriv 𝕜 b (fun x => c) x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0
case h₀
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : F →L[𝕜] G
u : α → F
x : α
hu : ContDiff 𝕜 (↑n) u
b : ℕ
a✝ : b ∈ Finset.range (n + 1)
hb : b ≠ 0
⊢ ↑(Nat.choose n b) * ‖0 x‖ * ‖iteratedFDeriv 𝕜 (n - b) u x‖ = 0