rcases h_ind with ⟨k_i, C_i, ⟨hC_i_nonneg, hC_i⟩⟩
case succ.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
k_m : ℕ
C_m : ℝ
hC_m : ∀ (x : E), f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
case succ.intro.intro.intro.intro.intro
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
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k