refine le_trans ?_ hC
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
k n : ℕ
C : ℝ
x : E
hC : (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ C
⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ ≤ (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ n f x‖