awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
a : EReal
⊢ (expGrowthInf fun (n : ℕ) ↦ (a * (↑n : EReal)).exp) = a

Tactic:
le_antisymm (Frequently.expGrowthInf_le (Frequently.of_forall fun _ ↦ le_refl _))
    (Eventually.le_expGrowthInf (Eventually.of_forall fun _ ↦ le_refl _))

Premises used: le_refl, HMul.hMul, Filter.Frequently.of_forall, Filter.Eventually.of_forall, Frequently.expGrowthInf_le, Nat.cast, le_antisymm, EReal.exp, Eventually.le_expGrowthInf
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
a : EReal
⊢ (expGrowthSup fun (n : ℕ) ↦ (a * (↑n : EReal)).exp) = a

Tactic:
le_antisymm (Eventually.expGrowthSup_le (Eventually.of_forall fun _ ↦ le_refl _))
    (Frequently.le_expGrowthSup (Frequently.of_forall fun _ ↦ le_refl _))

Premises used: le_refl, HMul.hMul, Filter.Frequently.of_forall, Filter.Eventually.of_forall, Nat.cast, le_antisymm, Frequently.le_expGrowthSup, EReal.exp, Eventually.expGrowthSup_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v)

Tactic:
le_liminf_add.trans_eq (liminf_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: ExpGrowth.expGrowthInf, LE.le.trans_eq, EReal.le_liminf_add, Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
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)
⊢ expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v)

Tactic:
refine le_liminf_add.trans_eq (liminf_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: LE.le.trans_eq, EReal.le_liminf_add, Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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)
rw₃ rw₄ : ((u n).log + (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)

Tactic:
rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]

Premises used: Pi.mul_apply, Nat.cast_nonneg', Pi.add_apply, EReal.add_div_of_nonneg_right, ENNReal.log_mul_add
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v

Tactic:
(liminf_add_le h h').trans_eq' (liminf_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: ExpGrowth.expGrowthInf, LE.le.trans_eq', EReal.liminf_add_le, Filter.Eventually.of_forall, Filter.liminf_congr, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
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)
⊢ expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v

Tactic:
refine (liminf_add_le h h').trans_eq' (liminf_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: LE.le.trans_eq', EReal.liminf_add_le, Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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)
rw₃ rw₄ : ((u n).log + (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)

Tactic:
rw [Pi.add_apply, Pi.mul_apply, ← add_div_of_nonneg_right n.cast_nonneg', log_mul_add]

Premises used: Pi.mul_apply, Nat.cast_nonneg', Pi.add_apply, EReal.add_div_of_nonneg_right, ENNReal.log_mul_add
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
rw : expGrowthInf (v * u) ≤ expGrowthSup v + expGrowthInf u
⊢ expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v

Tactic:
rw [mul_comm, add_comm]

Premises used: add_comm, mul_comm
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (v * u) ≤ expGrowthSup v + expGrowthInf u

Tactic:
expGrowthInf_mul_le h'.symm h.symm

Premises used: ExpGrowth.expGrowthInf_mul_le, Or.symm
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (v * u) ≤ expGrowthSup v + expGrowthInf u

Tactic:
exact expGrowthInf_mul_le h'.symm h.symm

Premises used: ExpGrowth.expGrowthInf_mul_le, Or.symm
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)

Tactic:
le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: ExpGrowth.expGrowthInf, LE.le.trans_eq, Filter.Eventually.of_forall, EReal.le_limsup_add, Filter.limsup_congr, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
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)
⊢ expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)

Tactic:
refine le_limsup_add.trans_eq (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: LE.le.trans_eq, Filter.Eventually.of_forall, EReal.le_limsup_add, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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)
rw₃ rw₄ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n).log / (↑n : EReal) + (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)

Tactic:
rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']

Premises used: Pi.mul_apply, Nat.cast_nonneg', Pi.add_apply, EReal.add_div_of_nonneg_right, ENNReal.log_mul_add
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
rw : expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)
⊢ expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v)

Tactic:
rw [mul_comm, add_comm]

Premises used: add_comm, mul_comm
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)

Tactic:
le_expGrowthSup_mul

Premises used: ExpGrowth.le_expGrowthSup_mul
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
⊢ expGrowthSup v + expGrowthInf u ≤ expGrowthSup (v * u)

Tactic:
exact le_expGrowthSup_mul

Premises used: ExpGrowth.le_expGrowthSup_mul
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

Tactic:
(limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: LE.le.trans_eq', Filter.Eventually.of_forall, Filter.limsup_congr, ExpGrowth.expGrowthSup, EReal.limsup_add_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
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)
⊢ expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

Tactic:
refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Premises used: LE.le.trans_eq', Filter.Eventually.of_forall, Filter.limsup_congr, EReal.limsup_add_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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)
rw₃ rw₄ : (u n).log / (↑n : EReal) + (v n).log / (↑n : EReal) = (u n).log / (↑n : EReal) + (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)

Tactic:
rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']

Premises used: Pi.mul_apply, Nat.cast_nonneg', Pi.add_apply, EReal.add_div_of_nonneg_right, ENNReal.log_mul_add
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
rw : expGrowthInf u⁻¹ = liminf (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop
⊢ expGrowthInf u⁻¹ = -expGrowthSup u

Tactic:
rw [expGrowthSup, ← liminf_neg]

Premises used: EReal.liminf_neg, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = liminf (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop

Tactic:
liminf_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: ExpGrowth.expGrowthInf, Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
refine : ∀ (n : ℕ), (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
⊢ expGrowthInf u⁻¹ = liminf (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop

Tactic:
refine liminf_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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)⁻¹
rw₅ rw₆ : -(u n).log * (↑n : EReal)⁻¹ = -(u n).log * (↑n : EReal)⁻¹
⊢ (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n

Tactic:
rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]

Premises used: div_eq_mul_inv, ENNReal.log_inv, EReal.neg_mul, Pi.neg_apply, Pi.inv_apply
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
rw : expGrowthSup u⁻¹ = limsup (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop
⊢ expGrowthSup u⁻¹ = -expGrowthInf u

Tactic:
rw [expGrowthInf, ← limsup_neg]

Premises used: ExpGrowth.expGrowthInf, EReal.limsup_neg
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = limsup (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop

Tactic:
limsup_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.limsup_congr, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u : ℕ → ℝ≥0∞
refine : ∀ (n : ℕ), (u⁻¹ n).log / (↑n : EReal) = (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) n
⊢ expGrowthSup u⁻¹ = limsup (β := ℕ) (-fun (n : ℕ) ↦ (u n).log / (↑n : EReal)) atTop

Tactic:
refine limsup_congr (Eventually.of_forall fun n ↦ ?_)

Premises used: Filter.Eventually.of_forall, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
apply : (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_eventually_monotone h).trans

Premises used: ExpGrowth.expGrowthInf_eventually_monotone, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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
inr : ∀ (b_pos : 0 < b), (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v
⊢ (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v

Tactic:
rcases eq_zero_or_pos b with rfl | b_pos

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) 0 ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthInf fun (x : ℕ) ↦ 0 * v x) ≤ expGrowthInf v

Tactic:
simp only [zero_mul, ← Pi.zero_def, expGrowthInf_zero, bot_le]

Premises used: MulZeroClass.zero_mul, Pi.zero_def, ExpGrowth.expGrowthInf_zero, bot_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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 ≠ ⊤
apply₁ : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
⊢ (expGrowthInf fun (x : ℕ) ↦ b * v x) ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_mul_le _ _).trans_eq

Premises used: LE.le.trans_eq, ExpGrowth.expGrowthInf_mul_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
inr : 0 + expGrowthInf v = expGrowthInf v
⊢ (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthInf v = expGrowthInf v

Tactic:
rw [expGrowthSup_const b_pos.ne' hb]

Premises used: ExpGrowth.expGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
rw : Ne (α := EReal) 0 ⊥ ∨ expGrowthInf v ≠ ⊤
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthInf v ≠ ⊤

Tactic:
rw [expGrowthSup_const b_pos.ne' hb]

Premises used: ExpGrowth.expGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
rw : Ne (α := EReal) 0 ⊤ ∨ expGrowthInf v ≠ ⊥
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthInf v ≠ ⊥

Tactic:
rw [expGrowthSup_const b_pos.ne' hb]

Premises used: ExpGrowth.expGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ 0 + expGrowthInf v = expGrowthInf v

Tactic:
zero_add (expGrowthInf v)

Premises used: ExpGrowth.expGrowthInf, zero_add
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ 0 + expGrowthInf v = expGrowthInf v

Tactic:
exact zero_add (expGrowthInf v)

Premises used: ExpGrowth.expGrowthInf, zero_add
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊥ ∨ expGrowthInf v ≠ ⊤

Tactic:
.inl zero_ne_bot

Premises used: EReal.zero_ne_bot, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊥ ∨ expGrowthInf v ≠ ⊤

Tactic:
exact .inl zero_ne_bot
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊤ ∨ expGrowthInf v ≠ ⊥

Tactic:
.inl zero_ne_top

Premises used: EReal.zero_ne_top, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊤ ∨ expGrowthInf v ≠ ⊥

Tactic:
exact .inl zero_ne_top
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
apply : (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
⊢ expGrowthSup u ≤ expGrowthSup v

Tactic:
apply (expGrowthSup_eventually_monotone h).trans

Premises used: ExpGrowth.expGrowthSup_eventually_monotone, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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
inr : ∀ (b_pos : 0 < b), (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v
⊢ (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v

Tactic:
rcases eq_zero_or_pos b with rfl | b_pos

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) 0 ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ 0 * v n
⊢ (expGrowthSup fun (x : ℕ) ↦ 0 * v x) ≤ expGrowthSup v

Tactic:
simp only [zero_mul, ← Pi.zero_def, expGrowthSup_zero, bot_le]

Premises used: MulZeroClass.zero_mul, Pi.zero_def, ExpGrowth.expGrowthSup_zero, bot_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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 ≠ ⊤
apply₁ : (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ (expGrowthSup fun (x : ℕ) ↦ b * v x) ≤ expGrowthSup v

Tactic:
apply (expGrowthSup_mul_le _ _).trans_eq

Premises used: LE.le.trans_eq, ExpGrowth.expGrowthSup_mul_le
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
inr : 0 + expGrowthSup v = expGrowthSup v
⊢ (expGrowthSup fun (x : ℕ) ↦ b) + expGrowthSup v = expGrowthSup v

Tactic:
rw [expGrowthSup_const b_pos.ne' hb]

Premises used: ExpGrowth.expGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
rw : Ne (α := EReal) 0 ⊥ ∨ expGrowthSup v ≠ ⊤
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊥ ∨ expGrowthSup v ≠ ⊤

Tactic:
rw [expGrowthSup_const b_pos.ne' hb]

Premises used: ExpGrowth.expGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
rw : Ne (α := EReal) 0 ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ (expGrowthSup fun (x : ℕ) ↦ b) ≠ ⊤ ∨ expGrowthSup v ≠ ⊥

Tactic:
rw [expGrowthSup_const b_pos.ne' hb]

Premises used: ExpGrowth.expGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ 0 + expGrowthSup v = expGrowthSup v

Tactic:
zero_add (expGrowthSup v)

Premises used: zero_add, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ 0 + expGrowthSup v = expGrowthSup v

Tactic:
exact zero_add (expGrowthSup v)

Premises used: zero_add, ExpGrowth.expGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊥ ∨ expGrowthSup v ≠ ⊤

Tactic:
.inl zero_ne_bot

Premises used: EReal.zero_ne_bot, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊥ ∨ expGrowthSup v ≠ ⊤

Tactic:
exact .inl zero_ne_bot
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊤ ∨ expGrowthSup v ≠ ⊥

Tactic:
.inl zero_ne_top

Premises used: EReal.zero_ne_top, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
b_pos : 0 < b
⊢ Ne (α := EReal) 0 ⊤ ∨ expGrowthSup v ≠ ⊥

Tactic:
exact .inl zero_ne_top
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
apply : expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_eventually_monotone h).trans' (le_expGrowthInf_mul.trans' _)

Premises used: ExpGrowth.expGrowthInf_eventually_monotone, ExpGrowth.le_expGrowthInf_mul, LE.le.trans'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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
inr : ∀ (b_top : b < ∞), expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u

Tactic:
rcases eq_top_or_lt_top b with rfl | b_top

Premises used: eq_top_or_lt_top, rfl
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) ∞ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
inl : expGrowthInf u ≤ ⊤ + expGrowthInf u
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthInf u

Tactic:
rw [← Pi.top_def, expGrowthInf_top]

Premises used: Pi.top_def, ExpGrowth.expGrowthInf_top
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) ∞ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
⊢ expGrowthInf u ≤ ⊤ + expGrowthInf u

Tactic:
le_add_of_nonneg_left le_top

Premises used: le_top, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
hb : Ne (α := ℝ≥0∞) ∞ 0
h : ∀ᶠ (n : ℕ) in atTop, ∞ * u n ≤ v n
⊢ expGrowthInf u ≤ ⊤ + expGrowthInf u

Tactic:
exact le_add_of_nonneg_left le_top

Premises used: le_top, le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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
inr₁ inr₂ : expGrowthInf u ≤ expGrowthInf u
⊢ expGrowthInf u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthInf u

Tactic:
rw [expGrowthInf_const hb b_top.ne, zero_add]

Premises used: zero_add, ExpGrowth.expGrowthInf_const, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
Goal:
u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, b * u n ≤ v n
apply : expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
⊢ expGrowthSup u ≤ expGrowthSup v

Tactic:
apply (expGrowthSup_eventually_monotone h).trans' (le_expGrowthSup_mul'.trans' _)

Premises used: ExpGrowth.expGrowthSup_eventually_monotone, ExpGrowth.le_expGrowthSup_mul', LE.le.trans'
-- Module: Mathlib.Analysis.Asymptotics.ExpGrowth
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),
    expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ ∞) + expGrowthSup u
inr : ∀ (b_top : b < ∞), expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u
⊢ expGrowthSup u ≤ (expGrowthInf fun (x : ℕ) ↦ b) + expGrowthSup u

Tactic:
rcases eq_top_or_lt_top b with rfl | b_top

Premises used: eq_top_or_lt_top, rfl