refine ⟨0, C, ?_⟩
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∃ k C, ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ k
case intro
E : Type u_1
F : Type u_2
G : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
n : ℕ
C : ℝ
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n f.toFun x‖ ≤ C
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ 0