awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (v + u) ≤ linearGrowthSup v + linearGrowthInf u

Tactic:
linearGrowthInf_add_le h'.symm h.symm

Premises used: Or.symm, LinearGrowth.linearGrowthInf_add_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (v + u) ≤ linearGrowthSup v + linearGrowthInf u

Tactic:
exact linearGrowthInf_add_le h'.symm h.symm

Premises used: Or.symm, LinearGrowth.linearGrowthInf_add_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
⊢ linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (u + v)

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

Premises used: LE.le.trans_eq, Filter.Eventually.of_forall, LinearGrowth.linearGrowthSup, LinearGrowth.linearGrowthInf, EReal.le_limsup_add, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
refine :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal))
        n =
      (u + v) n / (↑n : EReal)
⊢ linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (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.LinearGrowth
Goal:
u v : ℕ → EReal
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
rw₂ rw₃ : u n / (↑n : EReal) + v n / (↑n : EReal) = u n / (↑n : EReal) + v n / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)

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

Premises used: Nat.cast_nonneg', Pi.add_apply, EReal.add_div_of_nonneg_right
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
rw : linearGrowthSup v + linearGrowthInf u ≤ linearGrowthSup (v + u)
⊢ linearGrowthInf u + linearGrowthSup v ≤ linearGrowthSup (u + v)

Tactic:
rw [add_comm u v, add_comm (linearGrowthInf u) (linearGrowthSup v)]

Premises used: add_comm, LinearGrowth.linearGrowthSup, LinearGrowth.linearGrowthInf
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
⊢ linearGrowthSup v + linearGrowthInf u ≤ linearGrowthSup (v + u)

Tactic:
le_linearGrowthSup_add

Premises used: LinearGrowth.le_linearGrowthSup_add
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
⊢ linearGrowthSup v + linearGrowthInf u ≤ linearGrowthSup (v + u)

Tactic:
exact le_linearGrowthSup_add

Premises used: LinearGrowth.le_linearGrowthSup_add
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthSup (u + v) ≤ linearGrowthSup u + linearGrowthSup 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, LinearGrowth.linearGrowthSup, Filter.limsup_congr, EReal.limsup_add_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
refine :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal))
        n =
      (u + v) n / (↑n : EReal)
⊢ linearGrowthSup (u + v) ≤ linearGrowthSup u + linearGrowthSup 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.LinearGrowth
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
n : ℕ
rw : u n / (↑n : EReal) + v n / (↑n : EReal) = (u + v) n / (↑n : EReal)
rw₁ : u n / (↑n : EReal) + v n / (↑n : EReal) = (u n + v n) / (↑n : EReal)
rw₂ rw₃ : u n / (↑n : EReal) + v n / (↑n : EReal) = u n / (↑n : EReal) + v n / (↑n : EReal)
⊢ HAdd.hAdd (α := ℕ → EReal) (β := ℕ → EReal) (fun (n : ℕ) ↦ u n / (↑n : EReal)) (fun (n : ℕ) ↦ v n / (↑n : EReal)) n =
    (u + v) n / (↑n : EReal)

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

Premises used: Nat.cast_nonneg', Pi.add_apply, EReal.add_div_of_nonneg_right
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
rw : linearGrowthInf (-u) = liminf (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop
⊢ linearGrowthInf (-u) = -linearGrowthSup u

Tactic:
rw [linearGrowthSup, ← liminf_neg]

Premises used: EReal.liminf_neg, LinearGrowth.linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
⊢ linearGrowthInf (-u) = liminf (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop

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

Premises used: Filter.Eventually.of_forall, Filter.liminf_congr, LinearGrowth.linearGrowthInf
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
refine : ∀ (n : ℕ), (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
⊢ linearGrowthInf (-u) = liminf (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑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.LinearGrowth
Goal:
u : ℕ → EReal
n : ℕ
rw : -u n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
rw₁ : -u n / (↑n : EReal) = -(u n / (↑n : EReal))
rw₂ : -u n * (↑n : EReal)⁻¹ = -(u n / (↑n : EReal))
rw₃ : -u n * (↑n : EReal)⁻¹ = -(u n * (↑n : EReal)⁻¹)
rw₄ rw₅ : -u n * (↑n : EReal)⁻¹ = -u n * (↑n : EReal)⁻¹
⊢ (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n

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

Premises used: div_eq_mul_inv, neg_mul, Pi.neg_apply
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
rw : linearGrowthSup (-u) = limsup (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop
⊢ linearGrowthSup (-u) = -linearGrowthInf u

Tactic:
rw [linearGrowthInf, ← limsup_neg]

Premises used: EReal.limsup_neg, LinearGrowth.linearGrowthInf
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
⊢ linearGrowthSup (-u) = limsup (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑n : EReal)) atTop

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

Premises used: Filter.Eventually.of_forall, LinearGrowth.linearGrowthSup, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
refine : ∀ (n : ℕ), (-u) n / (↑n : EReal) = (-fun (n : ℕ) ↦ u n / (↑n : EReal)) n
⊢ linearGrowthSup (-u) = limsup (β := ℕ) (-fun (n : ℕ) ↦ u n / (↑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.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
apply : (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
⊢ linearGrowthInf u ≤ linearGrowthInf v

Tactic:
apply (linearGrowthInf_eventually_monotone h).trans

Premises used: LinearGrowth.linearGrowthInf_eventually_monotone, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
inl :
  ∀ (hb : Ne (α := EReal) ⊥ ⊤) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥),
    (linearGrowthInf fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthInf v
inr : ∀ (b_bot : ⊥ < b), (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v

Tactic:
rcases eq_bot_or_bot_lt b with rfl | b_bot

Premises used: eq_bot_or_bot_lt, rfl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
hb : Ne (α := EReal) ⊥ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthInf v

Tactic:
simp only [add_bot, ← Pi.bot_def, linearGrowthInf_bot, bot_le]

Premises used: LinearGrowth.linearGrowthInf_bot, EReal.add_bot, Pi.bot_def, bot_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : (linearGrowthInf v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthInf v
apply : linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
apply₁ : linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥
⊢ (linearGrowthInf fun (x : ℕ) ↦ v x + b) ≤ linearGrowthInf v

Tactic:
apply (linearGrowthInf_add_le' _ _).trans_eq

Premises used: LinearGrowth.linearGrowthInf_add_le', LE.le.trans_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : linearGrowthInf v + 0 = linearGrowthInf v
⊢ (linearGrowthInf v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthInf v

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Premises used: LinearGrowth.linearGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
rw : linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤
⊢ linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Premises used: LinearGrowth.linearGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
rw : linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥
⊢ linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Premises used: LinearGrowth.linearGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v + 0 = linearGrowthInf v

Tactic:
add_zero (linearGrowthInf v)

Premises used: LinearGrowth.linearGrowthInf, add_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v + 0 = linearGrowthInf v

Tactic:
exact add_zero (linearGrowthInf v)

Premises used: LinearGrowth.linearGrowthInf, add_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤

Tactic:
Or.inr EReal.zero_ne_top

Premises used: EReal.zero_ne_top, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤

Tactic:
exact Or.inr EReal.zero_ne_top

Premises used: EReal.zero_ne_top, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥

Tactic:
Or.inr EReal.zero_ne_bot

Premises used: EReal.zero_ne_bot, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥

Tactic:
exact Or.inr EReal.zero_ne_bot

Premises used: EReal.zero_ne_bot, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
apply : (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
⊢ linearGrowthSup u ≤ linearGrowthSup v

Tactic:
apply (linearGrowthSup_eventually_monotone h).trans

Premises used: LinearGrowth.linearGrowthSup_eventually_monotone, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
inl :
  ∀ (hb : Ne (α := EReal) ⊥ ⊤) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥),
    (linearGrowthSup fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthSup v
inr : ∀ (b_bot : ⊥ < b), (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v

Tactic:
rcases eq_bot_or_bot_lt b with rfl | b_bot

Premises used: eq_bot_or_bot_lt, rfl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
hb : Ne (α := EReal) ⊥ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthSup v

Tactic:
simp only [add_bot, ← Pi.bot_def, linearGrowthSup_bot, bot_le]

Premises used: LinearGrowth.linearGrowthSup_bot, EReal.add_bot, Pi.bot_def, bot_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : (linearGrowthSup v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthSup v
apply : linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
apply₁ : linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v

Tactic:
apply (linearGrowthSup_add_le _ _).trans_eq

Premises used: LinearGrowth.linearGrowthSup_add_le, LE.le.trans_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : linearGrowthSup v + 0 = linearGrowthSup v
⊢ (linearGrowthSup v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthSup v

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Premises used: LinearGrowth.linearGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
rw : linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤
⊢ linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Premises used: LinearGrowth.linearGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
rw : linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥
⊢ linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥

Tactic:
rw [linearGrowthSup_const b_bot.ne' hb]

Premises used: LinearGrowth.linearGrowthSup_const, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v + 0 = linearGrowthSup v

Tactic:
add_zero (linearGrowthSup v)

Premises used: LinearGrowth.linearGrowthSup, add_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v + 0 = linearGrowthSup v

Tactic:
exact add_zero (linearGrowthSup v)

Premises used: LinearGrowth.linearGrowthSup, add_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤

Tactic:
Or.inr EReal.zero_ne_top

Premises used: EReal.zero_ne_top, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤

Tactic:
exact Or.inr EReal.zero_ne_top

Premises used: EReal.zero_ne_top, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥

Tactic:
Or.inr EReal.zero_ne_bot

Premises used: EReal.zero_ne_bot, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥

Tactic:
exact Or.inr EReal.zero_ne_bot

Premises used: EReal.zero_ne_bot, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
rw :
  Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (u ⊓ v) n / (↑n : EReal)) atTop)
    (liminf (fun (a : ℕ) ↦ min (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)
⊢ linearGrowthInf (u ⊓ v) = min (linearGrowthInf u) (linearGrowthInf v)

Tactic:
rw [linearGrowthInf, linearGrowthInf, linearGrowthInf, ← liminf_min]

Premises used: LinearGrowth.linearGrowthInf, liminf_min
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (u ⊓ v) n / (↑n : EReal)) atTop)
    (liminf (fun (a : ℕ) ↦ min (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)

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

Premises used: Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
refine : ∀ (n : ℕ), (u ⊓ v) n / (↑n : EReal) = min (u n / (↑n : EReal)) (v n / (↑n : EReal))
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (u ⊓ v) n / (↑n : EReal)) atTop)
    (liminf (fun (a : ℕ) ↦ min (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)

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

Premises used: Filter.Eventually.of_forall, Filter.liminf_congr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
n : ℕ
⊢ (u ⊓ v) n / (↑n : EReal) = min (u n / (↑n : EReal)) (v n / (↑n : EReal))

Tactic:
(monotone_div_right_of_nonneg n.cast_nonneg').map_min

Premises used: Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Monotone.map_min
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
n : ℕ
⊢ (u ⊓ v) n / (↑n : EReal) = min (u n / (↑n : EReal)) (v n / (↑n : EReal))

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_min

Premises used: Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg, Monotone.map_min
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ Eq (α := EReal) ((linearGrowthInfTopHom : (a : ℕ → EReal) → EReal) (hs.toFinset (s := s).inf u) : EReal)
    (hs.toFinset (s := s).inf ((⇑linearGrowthInfTopHom : (a : ℕ → EReal) → EReal) ∘ u) : EReal)

Tactic:
have := map_finset_inf linearGrowthInfTopHom hs.toFinset u
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
this :
  Eq (α := EReal) ((linearGrowthInfTopHom : (a : ℕ → EReal) → EReal) (hs.toFinset (s := s).inf u) : EReal)
    (hs.toFinset (s := s).inf ((⇑linearGrowthInfTopHom : (a : ℕ → EReal) → EReal) ∘ u) : EReal)
⊢ Eq (α := EReal) (linearGrowthInf (⨅ x ∈ s, u x)) (⨅ x ∈ s, linearGrowthInf (u x))

Tactic:
simpa only [linearGrowthInfTopHom, InfTopHom.coe_mk, InfHom.coe_mk, Finset.inf_eq_iInf,
    hs.mem_toFinset, comp_apply]

Premises used: Set.Finite.mem_toFinset, InfHom.coe_mk, InfTopHom.coe_mk, LinearGrowth.linearGrowthInfTopHom, Finset.inf_eq_iInf, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
rw :
  Eq (α := EReal) (linearGrowthInf (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
    (⨅ (i : ι), linearGrowthInf (u i))
rw₁ :
  Eq (α := EReal) (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), linearGrowthInf (u x))
    (⨅ (i : ι), linearGrowthInf (u i))
rw₂ rw₃ : Eq (α := EReal) (⨅ (x : ι), linearGrowthInf (u x)) (⨅ (i : ι), linearGrowthInf (u i))
⊢ Eq (α := EReal) (linearGrowthInf (⨅ (i : ι), u i)) (⨅ (i : ι), linearGrowthInf (u i))

Tactic:
rw [← iInf_univ, linearGrowthInf_biInf u Set.finite_univ, iInf_univ]

Premises used: LinearGrowth.linearGrowthInf_biInf, Set.finite_univ, iInf_univ
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
rw :
  Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (u ⊔ v) n / (↑n : EReal)) atTop)
    (limsup (fun (a : ℕ) ↦ max (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)
⊢ linearGrowthSup (u ⊔ v) = max (linearGrowthSup u) (linearGrowthSup v)

Tactic:
rw [linearGrowthSup, linearGrowthSup, linearGrowthSup, ← limsup_max]

Premises used: LinearGrowth.linearGrowthSup, limsup_max
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (u ⊔ v) n / (↑n : EReal)) atTop)
    (limsup (fun (a : ℕ) ↦ max (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)

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

Premises used: Filter.Eventually.of_forall, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
refine : ∀ (n : ℕ), (u ⊔ v) n / (↑n : EReal) = max (u n / (↑n : EReal)) (v n / (↑n : EReal))
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (u ⊔ v) n / (↑n : EReal)) atTop)
    (limsup (fun (a : ℕ) ↦ max (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)

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

Premises used: Filter.Eventually.of_forall, Filter.limsup_congr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
n : ℕ
⊢ (u ⊔ v) n / (↑n : EReal) = max (u n / (↑n : EReal)) (v n / (↑n : EReal))

Tactic:
(monotone_div_right_of_nonneg n.cast_nonneg').map_max

Premises used: Monotone.map_max, Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
n : ℕ
⊢ (u ⊔ v) n / (↑n : EReal) = max (u n / (↑n : EReal)) (v n / (↑n : EReal))

Tactic:
exact (monotone_div_right_of_nonneg n.cast_nonneg').map_max

Premises used: Monotone.map_max, Nat.cast_nonneg', EReal.monotone_div_right_of_nonneg
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ Eq (α := EReal) ((linearGrowthSupBotHom : (a : ℕ → EReal) → EReal) (hs.toFinset (s := s).sup u) : EReal)
    (hs.toFinset (s := s).sup ((⇑linearGrowthSupBotHom : (a : ℕ → EReal) → EReal) ∘ u) : EReal)

Tactic:
have := map_finset_sup linearGrowthSupBotHom hs.toFinset u
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
this :
  Eq (α := EReal) ((linearGrowthSupBotHom : (a : ℕ → EReal) → EReal) (hs.toFinset (s := s).sup u) : EReal)
    (hs.toFinset (s := s).sup ((⇑linearGrowthSupBotHom : (a : ℕ → EReal) → EReal) ∘ u) : EReal)
⊢ Eq (α := EReal) (linearGrowthSup (⨆ x ∈ s, u x)) (⨆ x ∈ s, linearGrowthSup (u x))

Tactic:
simpa only [linearGrowthSupBotHom, SupBotHom.coe_mk, SupHom.coe_mk, Finset.sup_eq_iSup,
    hs.mem_toFinset, comp_apply]

Premises used: Set.Finite.mem_toFinset, LinearGrowth.linearGrowthSupBotHom, Finset.sup_eq_iSup, SupHom.coe_mk, Function.comp_apply, SupBotHom.coe_mk
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
rw :
  Eq (α := EReal) (linearGrowthSup (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
    (⨆ (i : ι), linearGrowthSup (u i))
rw₁ :
  Eq (α := EReal) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), linearGrowthSup (u x))
    (⨆ (i : ι), linearGrowthSup (u i))
rw₂ rw₃ : Eq (α := EReal) (⨆ (x : ι), linearGrowthSup (u x)) (⨆ (i : ι), linearGrowthSup (u i))
⊢ Eq (α := EReal) (linearGrowthSup (⨆ (i : ι), u i)) (⨆ (i : ι), linearGrowthSup (u i))

Tactic:
rw [← iSup_univ, linearGrowthSup_biSup u Set.finite_univ, iSup_univ]

Premises used: LinearGrowth.linearGrowthSup_biSup, iSup_univ, Set.finite_univ
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

Tactic:
(eventually_ge_atTop (b - a)⁻¹).mono fun x ab_x ↦ ?_

Premises used: HSub.hSub, Filter.Eventually.mono, Inv.inv, Filter.eventually_ge_atTop