Theorem: bound_forall_range (ForML/HasTemperateGrowth.lean)

State before:
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
Tactic:
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
State after:
no goals

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

State before:
case zero
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℕ → E → ℝ
h : ∀ i < Nat.zero, ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ C, 0 ≤ C
Tactic:
use 0
State after:
no goals

State before:
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
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
specialize h_ind ?_
State after:
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

State before:
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
Tactic:
. intro i hi
  refine h _ ?_
  exact lt_trans hi (Nat.lt_succ_self _)
State after:
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

State before:
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
Tactic:
specialize h n (Nat.lt_succ_self _)
State after:
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 : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∃ k C, ∀ (x : E), f n x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k

State before:
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 : ∃ k C, 0 ≤ C ∧ ∀ i < n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
h : ∃ k C, ∀ (x : E), f n x ≤ C * (1 + ‖x‖) ^ k
⊢ ∃ k C, 0 ≤ C ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
rcases h with ⟨k_m, C_m, hC_m⟩
State after:
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

State before:
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
Tactic:
rcases h_ind with ⟨k_i, C_i, ⟨hC_i_nonneg, hC_i⟩⟩
State after:
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

State before:
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
Tactic:
refine ⟨max k_i k_m, max C_i C_m, ?_⟩
State after:
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
⊢ 0 ≤ max C_i C_m ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m

State before:
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
⊢ 0 ≤ max C_i C_m ∧ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine And.intro (le_trans hC_i_nonneg (by simp)) ?_
State after:
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
⊢ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m

State before:
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
⊢ ∀ i < Nat.succ n, ∀ (x : E), f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
intro i hi x
State after:
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
i : ℕ
hi : i < Nat.succ n
x : E
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m

State before:
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
i : ℕ
hi : i < Nat.succ n
x : E
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
simp [Nat.lt_succ] at hi
State after:
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
i : ℕ
x : E
hi : i ≤ n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m

State before:
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
i : ℕ
x : E
hi : i ≤ n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
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
State after:
no goals

State before:
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
Tactic:
intro i hi
State after:
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 : ℕ
hi : i < n
⊢ ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k

State before:
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 : ℕ
hi : i < n
⊢ ∃ k C, ∀ (x : E), f i x ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine h _ ?_
State after:
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 : ℕ
hi : i < n
⊢ i < Nat.succ n

State before:
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 : ℕ
hi : i < n
⊢ i < Nat.succ n
Tactic:
exact lt_trans hi (Nat.lt_succ_self _)
State after:
no goals

State before:
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
⊢ C_i ≤ max C_i C_m
Tactic:
simp
State after:
no goals

State before:
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
hC_i : ∀ i < n, ∀ (x : E), f i x ≤ C_i * (1 + ‖x‖) ^ k_i
i : ℕ
x : E
hi✝ : i ≤ n
hi : i < n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
specialize hC_i i hi x
State after:
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

State before:
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
Tactic:
refine le_trans hC_i ?_
State after:
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

State before:
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
Tactic:
refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
State after:
no goals

State before:
case succ.intro.intro.intro.intro.intro.inr
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
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
⊢ f i x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
rw [hi]
State after:
case succ.intro.intro.intro.intro.intro.inr
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
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m

State before:
case succ.intro.intro.intro.intro.intro.inr
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
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
specialize hC_m x
State after:
case succ.intro.intro.intro.intro.intro.inr
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 : ℝ
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
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m

State before:
case succ.intro.intro.intro.intro.intro.inr
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 : ℝ
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
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ f n x ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine le_trans hC_m ?_
State after:
case succ.intro.intro.intro.intro.intro.inr
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 : ℝ
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
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ C_m * (1 + ‖x‖) ^ k_m ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m

State before:
case succ.intro.intro.intro.intro.intro.inr
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 : ℝ
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
i : ℕ
x : E
hi✝ : i ≤ n
hi : i = n
hC_m : f n x ≤ C_m * (1 + ‖x‖) ^ k_m
⊢ C_m * (1 + ‖x‖) ^ k_m ≤ max C_i C_m * (1 + ‖x‖) ^ max k_i k_m
Tactic:
refine mul_le_mul ?_ (pow_le_pow_right ?_ ?_) ?_ (le_trans hC_i_nonneg ?_) <;> simp
State after:
no goals