simp at hC
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : (1 + ‖0‖) ^ k * ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C
case h.refine_1
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
r : ℝ
n k : ℕ
hk : ⌈r⌉₊ = k
C : ℝ
hC : ‖iteratedFDeriv ℝ n (⇑f) 0‖ ≤ C
⊢ 0 ≤ C