. intro i hi
  refine h _ ?_
  exact lt_trans hi (Nat.lt_succ_self _)
case succ
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 :
  (∀ 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
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∀ i < n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k

case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
case succ
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
n : ℕ
h : ∀ i < Nat.succ n, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h_ind : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k