awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
rw₂ : ((u n).log + (v n).log) / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₃ : ((u n).log + (v n).log) / (↑n : EReal) = ((u n).log + (v n).log) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
Tactic: refine (liminf_add_le h h').trans_eq' (liminf_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₂ : ((u n).log + (v n).log) / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
rw₂ : ((u n).log + (v n).log) / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₃ : ((u n).log + (v n).log) / (↑n : EReal) = ((u n).log + (v n).log) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v
have rw : expGrowthInf (v * u) ≤ expGrowthSup v + expGrowthInf u
Tactic: rw [mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
Tactic: refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₂ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u n).log + (v n).log) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
rw₂ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u n).log + (v n).log) / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₃ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v)
have rw : expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)
Tactic: rw [mul_comm, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v
have refine : ∀ (n : ℕ),
  HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
Tactic: refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₂ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u n).log + (v n).log) / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
rw : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u * v) n).log / (↑n : EReal)
rw₁ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n * v n).log / (↑n : EReal)
rw₂ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = ((u n).log + (v n).log) / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ (u n).log / (↑n : EReal))
      (fun (n : ℕ) ↦ (v n).log / (↑n : EReal)) n =
    ((u * v) n).log / (↑n : EReal)
have rw₃ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal)
Tactic: rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = -expGrowthSup u
have rw : expGrowthInf u⁻¹ = liminf (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop
Tactic: rw [expGrowthSup, ← liminf_neg]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = liminf (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop
have refine : ∀ (n : ℕ), (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
Tactic: refine liminf_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
n : ℕ
⊢ (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
have rw : (u⁻¹ n).log / (↑n : EReal) = -((u n).log / (↑n : EReal))
Tactic: rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
n : ℕ
rw : (u⁻¹ n).log / (↑n : EReal) = -((u n).log / (↑n : EReal))
⊢ (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
have rw₁ : (u n)⁻¹.log / (↑n : EReal) = -((u n).log / (↑n : EReal))
Tactic: rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
n : ℕ
rw : (u⁻¹ n).log / (↑n : EReal) = -((u n).log / (↑n : EReal))
rw₁ : (u n)⁻¹.log / (↑n : EReal) = -((u n).log / (↑n : EReal))
⊢ (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
have rw₂ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -((u n).log / (↑n : EReal))
Tactic: rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
n : ℕ
rw : (u⁻¹ n).log / (↑n : EReal) = -((u n).log / (↑n : EReal))
rw₁ : (u n)⁻¹.log / (↑n : EReal) = -((u n).log / (↑n : EReal))
rw₂ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -((u n).log / (↑n : EReal))
⊢ (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
have rw₃ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -((u n).log * (↑n : EReal)⁻¹)
Tactic: rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
n : ℕ
rw : (u⁻¹ n).log / (↑n : EReal) = -((u n).log / (↑n : EReal))
rw₁ : (u n)⁻¹.log / (↑n : EReal) = -((u n).log / (↑n : EReal))
rw₂ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -((u n).log / (↑n : EReal))
rw₃ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -((u n).log * (↑n : EReal)⁻¹)
⊢ (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
have rw₄ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -(u n).log * (↑n : EReal)⁻¹
Tactic: rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
n : ℕ
rw : (u⁻¹ n).log / (↑n : EReal) = -((u n).log / (↑n : EReal))
rw₁ : (u n)⁻¹.log / (↑n : EReal) = -((u n).log / (↑n : EReal))
rw₂ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -((u n).log / (↑n : EReal))
rw₃ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -((u n).log * (↑n : EReal)⁻¹)
rw₄ : (u n)⁻¹.log * (↑n : EReal)⁻¹ = -(u n).log * (↑n : EReal)⁻¹
⊢ (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
have rw₅ : -(u n).log * (↑n : EReal)⁻¹ = -(u n).log * (↑n : EReal)⁻¹
Tactic: rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = -expGrowthInf u
have rw : expGrowthSup u⁻¹ = limsup (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop
Tactic: rw [expGrowthInf, ← limsup_neg]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = limsup (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop
have refine : ∀ (n : ℕ), (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
Tactic: refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ expGrowthInf u ≤ expGrowthInf v
have apply : (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
Tactic: apply (expGrowthInf_eventually_monotone h).trans
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
have inl : ∀ (hb : Ne (α := ℝ≥0∞) 0 ∞) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n),
  (expGrowthInf fun (x : ℕ) ↦ 0 * v x) ≤ expGrowthInf v
Tactic: rcases eq_zero_or_pos b with rfl | b_pos
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
inl :
  ∀ (hb : Ne (α := ℝ≥0∞) 0 ∞) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n),
    (expGrowthInf fun (x : ℕ) ↦ 0 * v x) ≤ expGrowthInf v
⊢ (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
have inr : ∀ (b_pos : 0 < b), (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
Tactic: rcases eq_zero_or_pos b with rfl | b_pos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
have inr : (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthInf v = expGrowthInf v
Tactic: apply (expGrowthInf_mul_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
inr : (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthInf v = expGrowthInf v
⊢ (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
have apply : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
Tactic: apply (expGrowthInf_mul_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
inr : (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthInf v = expGrowthInf v
apply : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
⊢ (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
have apply₁ : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
Tactic: apply (expGrowthInf_mul_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthInf v = expGrowthInf v
have inr : 0 + expGrowthInf v = expGrowthInf v
Tactic: rw [expGrowthSup_const b_pos.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
have rw : Ne (α := EReal) 0 ⊥ ∨ expGrowthInf v ≠ ⊤
Tactic: rw [expGrowthSup_const b_pos.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
have rw : Ne (α := EReal) 0 ⊤ ∨ expGrowthInf v ≠ ⊥
Tactic: rw [expGrowthSup_const b_pos.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ expGrowthSup u ≤ expGrowthSup v
have apply : (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
Tactic: apply (expGrowthSup_eventually_monotone h).trans
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
have inl : ∀ (hb : Ne (α := ℝ≥0∞) 0 ∞) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n),
  (expGrowthSup fun (x : ℕ) ↦ 0 * v x) ≤ expGrowthSup v
Tactic: rcases eq_zero_or_pos b with rfl | b_pos
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
inl :
  ∀ (hb : Ne (α := ℝ≥0∞) 0 ∞) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n),
    (expGrowthSup fun (x : ℕ) ↦ 0 * v x) ≤ expGrowthSup v
⊢ (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
have inr : ∀ (b_pos : 0 < b), (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
Tactic: rcases eq_zero_or_pos b with rfl | b_pos
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
have inr : (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthSup v = expGrowthSup v
Tactic: apply (expGrowthSup_mul_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
inr : (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthSup v = expGrowthSup v
⊢ (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
have apply : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
Tactic: apply (expGrowthSup_mul_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
inr : (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthSup v = expGrowthSup v
apply : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
⊢ (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
have apply₁ : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
Tactic: apply (expGrowthSup_mul_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthSup v = expGrowthSup v
have inr : 0 + expGrowthSup v = expGrowthSup v
Tactic: rw [expGrowthSup_const b_pos.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
have rw : Ne (α := EReal) 0 ⊥ ∨ expGrowthSup v ≠ ⊤
Tactic: rw [expGrowthSup_const b_pos.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
have rw : Ne (α := EReal) 0 ⊤ ∨ expGrowthSup v ≠ ⊥
Tactic: rw [expGrowthSup_const b_pos.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthInf u ≤ expGrowthInf v
have apply : expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
Tactic: apply (expGrowthInf_eventually_monotone h).trans' (le_expGrowthInf_mul.trans' _)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
have inl : ∀ (hb : Ne (α := ℝ≥0∞) ∞ 0) (h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n),
  expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthInf u
Tactic: rcases eq_top_or_lt_top b with rfl | b_top
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
inl :
  ∀ (hb : Ne (α := ℝ≥0∞) ∞ 0) (h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n),
    expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthInf u
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
have inr : ∀ (b_top : b < ∞), expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
Tactic: rcases eq_top_or_lt_top b with rfl | b_top
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) ∞ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthInf u
have inl : expGrowthInf u ≤ ⊤ + expGrowthInf u
Tactic: rw [← Pi.top_def, expGrowthInf_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
have inr : expGrowthInf u ≤ 0 + expGrowthInf u
Tactic: rw [expGrowthInf_const hb b_top.ne, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
b_top : b < ∞
inr : expGrowthInf u ≤ 0 + expGrowthInf u
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
have inr₁ : expGrowthInf u ≤ expGrowthInf u
Tactic: rw [expGrowthInf_const hb b_top.ne, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.ExpGrowth (goal)
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
⊢ expGrowthSup u ≤ expGrowthSup v
have apply : expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
Tactic: apply (expGrowthSup_eventually_monotone h).trans' (le_expGrowthSup_mul'.trans' _)