refine le_trans hC_i ?_
case succ.intro.intro.intro.intro.intro.inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
hC_i : f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
case succ.intro.intro.intro.intro.intro.inl
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
k_i : ℕ
C_i : ℝ
hC_i_nonneg : 0 ≤ C_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
hC_i : f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ C_i * (1 + ‖x‖) ^ k_i ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m