induction n with
| zero => simp; use 0
| succ n h_ind =>
  specialize h_ind ?_  . intro i hi
    refine h _ ?_
    exact lt_trans hi (Nat.lt_succ_self _)
  specialize h n (Nat.lt_succ_self _)
  rcases h with ⟨k_m, C_m, hC_m⟩
  rcases h_ind with ⟨k_i, C_i, ⟨hC_i_nonneg, hC_i⟩⟩
  refine ⟨max k_i k_m, max C_i C_m, ?_⟩
  refine And.intro (le_trans hC_i_nonneg (by simp)) ?_
  intro i hi x
  simp [Nat.lt_succ] at hi
  cases lt_or_eq_of_le hi with
  | inl hi =>
    specialize hC_i i hi x
    refine le_trans hC_i ?_
    refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
  | inr hi =>
    rw [hi]
    specialize hC_m x
    refine le_trans hC_m ?_
    refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
f : ℕ → E → ℝ
h : ∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
no goals