awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)

Tactic:
forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
refine : ∀ b > a, ∀ n ≥ 1, u n / (↑n : EReal) ≤ b ↔ u n ≤ b * (↑n : EReal)
⊢ (∀ y > a, ∃ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)

Tactic:
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ LT.lt (α := EReal) 0 (↑n : EReal)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a b : EReal
h : b > a
n : ℕ
h_1 : n ≥ 1
rw : u n ≤ (↑n : EReal) * b ↔ u n ≤ b * (↑n : EReal)
rw₁ rw₂ : u n ≤ b * (↑n : EReal) ↔ u n ≤ b * (↑n : EReal)
⊢ u n / (↑n : EReal) ≤ b ↔ u n ≤ b * (↑n : EReal)

Tactic:
rw [div_le_iff_le_mul (by norm_cast) (natCast_ne_top n), mul_comm _ b]

Premises used: mul_comm, EReal.natCast_ne_top, EReal.div_le_iff_le_mul
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
rw : (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
⊢ a ≤ linearGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n

Tactic:
rw [linearGrowthInf, le_liminf_iff']

Premises used: Filter.le_liminf_iff', LinearGrowth.linearGrowthInf
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n

Tactic:
forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
refine : ∀ b < a, ∀ n ≥ 1, b ≤ u n / (↑n : EReal) ↔ b * (↑n : EReal) ≤ u n
⊢ (∀ y < a, ∀ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n

Tactic:
refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < n
⊢ GT.gt (α := EReal) (↑n : EReal) 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a b : EReal
h : b < a
n : ℕ
h_1 : n ≥ 1
nth_rw nth_rw₁ : b * (↑n : EReal) ≤ u n ↔ b * (↑n : EReal) ≤ u n
⊢ b ≤ u n / (↑n : EReal) ↔ b * (↑n : EReal) ≤ u n

Tactic:
nth_rw 1 [le_div_iff_mul_le (by norm_cast) (natCast_ne_top n)]

Premises used: EReal.natCast_ne_top, EReal.le_div_iff_mul_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
rw : (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)
⊢ linearGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)

Tactic:
rw [linearGrowthSup, limsup_le_iff']

Premises used: Filter.limsup_le_iff', LinearGrowth.linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)

Tactic:
forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
refine : ∀ b > a, ∀ n ≥ 1, u n / (↑n : EReal) ≤ b ↔ u n ≤ b * (↑n : EReal)
⊢ (∀ y > a, ∀ᶠ (a : ℕ) in atTop, u a / (↑a : EReal) ≤ y) ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * (↑n : EReal)

Tactic:
refine forall₂_congr fun b _ ↦ eventually_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.eventually_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
rw : (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n
⊢ a ≤ linearGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n

Tactic:
rw [linearGrowthSup, le_limsup_iff']

Premises used: Filter.le_limsup_iff', LinearGrowth.linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n

Tactic:
forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
refine : ∀ b < a, ∀ n ≥ 1, b ≤ u n / (↑n : EReal) ↔ b * (↑n : EReal) ≤ u n
⊢ (∀ y < a, ∃ᶠ (a : ℕ) in atTop, y ≤ u a / (↑a : EReal)) ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * (↑n : EReal) ≤ u n

Tactic:
refine forall₂_congr fun b _ ↦ frequently_congr (eventually_atTop.2 ⟨1, fun n _ ↦ ?_⟩)

Premises used: Iff.mpr, forall₂_congr, Exists.intro, Filter.frequently_congr, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : linearGrowthInf u < a
⊢ ∃ᶠ (n : ℕ) in atTop, u n ≤ a * (↑n : EReal)

Tactic:
linearGrowthInf_le_iff.1 (le_refl (linearGrowthInf u)) a h

Premises used: le_refl, LinearGrowth.linearGrowthInf, Iff.mp, LinearGrowth.linearGrowthInf_le_iff
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : a < linearGrowthInf u
⊢ ∀ᶠ (n : ℕ) in atTop, a * (↑n : EReal) ≤ u n

Tactic:
le_linearGrowthInf_iff.1 (le_refl (linearGrowthInf u)) a h

Premises used: le_refl, LinearGrowth.linearGrowthInf, LinearGrowth.le_linearGrowthInf_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : linearGrowthSup u < a
⊢ ∀ᶠ (n : ℕ) in atTop, u n ≤ a * (↑n : EReal)

Tactic:
linearGrowthSup_le_iff.1 (le_refl (linearGrowthSup u)) a h

Premises used: le_refl, LinearGrowth.linearGrowthSup_le_iff, LinearGrowth.linearGrowthSup, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : a < linearGrowthSup u
⊢ ∃ᶠ (n : ℕ) in atTop, a * (↑n : EReal) ≤ u n

Tactic:
le_linearGrowthSup_iff.1 (le_refl (linearGrowthSup u)) a h

Premises used: le_refl, LinearGrowth.linearGrowthSup, Iff.mp, LinearGrowth.le_linearGrowthSup_iff
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ a * (↑n : EReal)
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ a * (↑n : EReal)
ha : LE.le (α := EReal) 0 (↑n : EReal)
⊢ a * (↑n : EReal) ≤ c * (↑n : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, a * (↑n : EReal) ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : a * (↑n : EReal) ≤ u n
ha : LE.le (α := EReal) 0 (↑n : EReal)
⊢ c * (↑n : EReal) ≤ a * (↑n : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ a * (↑n : EReal)
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ a * (↑n : EReal)
ha : LE.le (α := EReal) 0 (↑n : EReal)
⊢ a * (↑n : EReal) ≤ c * (↑n : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, a * (↑n : EReal) ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : a * (↑n : EReal) ≤ u n
ha : LE.le (α := EReal) 0 (↑n : EReal)
⊢ c * (↑n : EReal) ≤ a * (↑n : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
nth_rw : Eq (α := EReal) (linearGrowthSup ⊥) (limsup (fun (x : ℕ) ↦ ⊥) atTop)
⊢ Eq (α := EReal) (linearGrowthSup ⊥) ⊥

Tactic:
nth_rw 2 [← limsup_const (f := atTop (α := ℕ)) ⊥]

Premises used: Filter.limsup_const, Bot.bot
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ Eq (α := EReal) (linearGrowthSup ⊥) (limsup (fun (x : ℕ) ↦ ⊥) atTop)

Tactic:
limsup_congr <| (eventually_gt_atTop 0).mono fun n n_pos ↦ ?_

Premises used: Filter.Eventually.mono, LinearGrowth.linearGrowthSup, Filter.limsup_congr, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
refine : ∀ (n : ℕ) (n_pos : 0 < n), HDiv.hDiv (α := EReal) (⊥ n) (↑n : EReal) = ⊥
⊢ Eq (α := EReal) (linearGrowthSup ⊥) (limsup (fun (x : ℕ) ↦ ⊥) atTop)

Tactic:
refine limsup_congr <| (eventually_gt_atTop 0).mono fun n n_pos ↦ ?_

Premises used: Filter.Eventually.mono, Filter.limsup_congr, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
n : ℕ
n_pos : 0 < n
⊢ LT.lt (α := EReal) 0 (↑n : EReal)

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
n : ℕ
n_pos : 0 < n
⊢ HDiv.hDiv (α := EReal) (⊥ n) (↑n : EReal) = ⊥

Tactic:
exact bot_div_of_pos_ne_top (by positivity) (natCast_ne_top n)

Premises used: EReal.bot_div_of_pos_ne_top, EReal.natCast_ne_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
apply : LE.le (α := EReal) (linearGrowthInf ⊥) ⊥
⊢ Eq (α := EReal) (linearGrowthInf ⊥) ⊥

Tactic:
apply le_bot_iff.1

Premises used: le_bot_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
rw : LE.le (α := EReal) (linearGrowthInf ⊥) (linearGrowthSup ⊥)
⊢ LE.le (α := EReal) (linearGrowthInf ⊥) ⊥

Tactic:
rw [← linearGrowthSup_bot]

Premises used: LinearGrowth.linearGrowthSup_bot
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ LE.le (α := EReal) (linearGrowthInf ⊥) (linearGrowthSup ⊥)

Tactic:
linearGrowthInf_le_linearGrowthSup

Premises used: LinearGrowth.linearGrowthInf_le_linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ LE.le (α := EReal) (linearGrowthInf ⊥) (linearGrowthSup ⊥)

Tactic:
exact linearGrowthInf_le_linearGrowthSup

Premises used: LinearGrowth.linearGrowthInf_le_linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
nth_rw : Eq (α := EReal) (linearGrowthInf ⊤) (liminf (fun (x : ℕ) ↦ ⊤) atTop)
⊢ Eq (α := EReal) (linearGrowthInf ⊤) ⊤

Tactic:
nth_rw 2 [← liminf_const (f := atTop (α := ℕ)) ⊤]

Premises used: Filter.liminf_const, Top.top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ Eq (α := EReal) (linearGrowthInf ⊤) (liminf (fun (x : ℕ) ↦ ⊤) atTop)

Tactic:
liminf_congr (eventually_atTop.2 ?_)

Premises used: Iff.mpr, Filter.liminf_congr, LinearGrowth.linearGrowthInf, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
refine : ∃ (a : ℕ), ∀ b ≥ a, HDiv.hDiv (α := EReal) (⊤ b) (↑b : EReal) = ⊤
⊢ Eq (α := EReal) (linearGrowthInf ⊤) (liminf (fun (x : ℕ) ↦ ⊤) atTop)

Tactic:
refine liminf_congr (eventually_atTop.2 ?_)

Premises used: Iff.mpr, Filter.liminf_congr, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ ∃ (a : ℕ), ∀ b ≥ a, HDiv.hDiv (α := EReal) (⊤ b) (↑b : EReal) = ⊤

Tactic:
⟨1, fun n n_pos ↦ top_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩

Premises used: Iff.mpr, EReal.top_div_of_pos_ne_top, Exists.intro, EReal.natCast_ne_top, OfNat.ofNat, Nat.cast_pos'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ ∃ (a : ℕ), ∀ b ≥ a, HDiv.hDiv (α := EReal) (⊤ b) (↑b : EReal) = ⊤

Tactic:
exact ⟨1, fun n n_pos ↦ top_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
apply : LE.le (α := EReal) ⊤ (linearGrowthSup ⊤)
⊢ Eq (α := EReal) (linearGrowthSup ⊤) ⊤

Tactic:
apply top_le_iff.1

Premises used: top_le_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
rw : LE.le (α := EReal) (linearGrowthInf ⊤) (linearGrowthSup ⊤)
⊢ LE.le (α := EReal) ⊤ (linearGrowthSup ⊤)

Tactic:
rw [← linearGrowthInf_top]

Premises used: LinearGrowth.linearGrowthInf_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ LE.le (α := EReal) (linearGrowthInf ⊤) (linearGrowthSup ⊤)

Tactic:
linearGrowthInf_le_linearGrowthSup

Premises used: LinearGrowth.linearGrowthInf_le_linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ LE.le (α := EReal) (linearGrowthInf ⊤) (linearGrowthSup ⊤)

Tactic:
exact linearGrowthInf_le_linearGrowthSup

Premises used: LinearGrowth.linearGrowthInf_le_linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
b : EReal
h : b ≠ ⊥
h' : b ≠ ⊤
⊢ Eq (α := EReal) (linearGrowthInf fun (x : ℕ) ↦ b) 0

Tactic:
(tendsto_const_div_atTop_nhds_zero_nat h h').liminf_eq

Premises used: EReal.tendsto_const_div_atTop_nhds_zero_nat, Filter.Tendsto.liminf_eq, LinearGrowth.linearGrowthInf
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
b : EReal
h : b ≠ ⊥
h' : b ≠ ⊤
⊢ Eq (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) 0

Tactic:
(tendsto_const_div_atTop_nhds_zero_nat h h').limsup_eq

Premises used: Filter.Tendsto.limsup_eq, EReal.tendsto_const_div_atTop_nhds_zero_nat, LinearGrowth.linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ Eq (α := EReal) (linearGrowthInf 0) 0

Tactic:
linearGrowthInf_const zero_ne_bot zero_ne_top

Premises used: EReal.zero_ne_bot, WithBot.some, LinearGrowth.linearGrowthInf_const, EReal.zero_ne_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
⊢ Eq (α := EReal) (linearGrowthSup 0) 0

Tactic:
linearGrowthSup_const zero_ne_bot zero_ne_top

Premises used: EReal.zero_ne_bot, WithBot.some, EReal.zero_ne_top, LinearGrowth.linearGrowthSup_const
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a : EReal
⊢ (linearGrowthInf fun (n : ℕ) ↦ a * (↑n : EReal)) = a

Tactic:
le_antisymm (Frequently.linearGrowthInf_le (Frequently.of_forall fun _ ↦ le_refl _))
    (Eventually.le_linearGrowthInf (Eventually.of_forall fun _ ↦ le_refl _))

Premises used: le_refl, HMul.hMul, Filter.Frequently.of_forall, Eventually.le_linearGrowthInf, Filter.Eventually.of_forall, Nat.cast, le_antisymm, Frequently.linearGrowthInf_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a : EReal
⊢ (linearGrowthSup fun (n : ℕ) ↦ a * (↑n : EReal)) = a

Tactic:
le_antisymm (Eventually.linearGrowthSup_le (Eventually.of_forall fun _ ↦ le_refl _))
    (Frequently.le_linearGrowthSup (Frequently.of_forall fun _ ↦ le_refl _))

Premises used: le_refl, HMul.hMul, Filter.Frequently.of_forall, Eventually.linearGrowthSup_le, Filter.Eventually.of_forall, Nat.cast, le_antisymm, Frequently.le_linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
v : ℕ → ℕ
⊢ LE.le (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))

Tactic:
(le_liminf_of_le) (Eventually.of_forall fun n ↦ div_nonneg (v n).cast_nonneg' n.cast_nonneg')

Premises used: Nat.cast_nonneg', Filter.Eventually.of_forall, LinearGrowth.linearGrowthInf, EReal.div_nonneg, Filter.le_liminf_of_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
obtain : ∀ (a : EReal) (a_0 : 0 < a) (a_v : a < linearGrowthInf u), Tendsto u atTop (𝓝 ⊤)
⊢ Tendsto u atTop (𝓝 ⊤)

Tactic:
obtain ⟨a, a_0, a_v⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
apply : Tendsto (β := EReal) (fun (x : ℕ) ↦ a * (↑x : EReal)) atTop (𝓝 ⊤)
⊢ Tendsto u atTop (𝓝 ⊤)

Tactic:
apply tendsto_nhds_top_mono _ ((le_linearGrowthInf_iff (u := u)).1 (le_refl _) a a_v)

Premises used: le_refl, tendsto_nhds_top_mono, LinearGrowth.le_linearGrowthInf_iff, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
⊢ Tendsto (β := EReal) (fun (x : ℕ) ↦ a * (↑x : EReal)) atTop (𝓝 ⊤)

Tactic:
tendsto_nhds_top_iff_real.2 fun M ↦ eventually_atTop.2 ?_

Premises used: Iff.mpr, EReal.tendsto_nhds_top_iff_real, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
refine : ∀ (M : ℝ), ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < a * (↑b : EReal)
⊢ Tendsto (β := EReal) (fun (x : ℕ) ↦ a * (↑x : EReal)) atTop (𝓝 ⊤)

Tactic:
refine tendsto_nhds_top_iff_real.2 fun M ↦ eventually_atTop.2 ?_

Premises used: Iff.mpr, EReal.tendsto_nhds_top_iff_real, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
M : ℝ
⊢ a ≠ ⊤ ∧ a ≠ ⊥

Tactic:
⟨ne_top_of_lt a_v, ne_bot_of_gt a_0⟩

Premises used: And.intro, ne_top_of_lt, ne_bot_of_gt
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf u
M : ℝ
lift :
  ∀ (a : ℝ) (a_0 : 0 < (↑a : EReal)) (a_v : (↑a : EReal) < linearGrowthInf u),
    ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < a * (↑b : EReal)

Tactic:
lift a to ℝ using ⟨ne_top_of_lt a_v, ne_bot_of_gt a_0⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < (↑a : EReal)
a_v : (↑a : EReal) < linearGrowthInf u
⊢ 0 < a

Tactic:
rw [EReal.coe_pos] at a_0

Premises used: EReal.coe_pos
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < (↑a : EReal)
a_v : (↑a : EReal) < linearGrowthInf u
a_0₁ : 0 < a
⊢ (↑a : EReal) < linearGrowthInf u

Tactic:
rw [EReal.coe_pos] at a_0

Premises used: EReal.coe_pos
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
obtain : ∀ (n : ℕ) (hn : M / a ≤ (↑n : ℝ)), ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)

Tactic:
obtain ⟨n, hn⟩ := exists_nat_ge (M / a)

Premises used: exists_nat_ge, HDiv.hDiv
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
n : ℕ
hn : M / a ≤ (↑n : ℝ)
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)

Tactic:
⟨n + 1, fun k k_n ↦ ?_⟩

Premises used: HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
n : ℕ
hn : M / a ≤ (↑n : ℝ)
refine : ∀ (k : ℕ) (k_n : k ≥ n + 1), (↑M : EReal) < (↑a : EReal) * (↑k : EReal)
⊢ ∃ (a_1 : ℕ), ∀ b ≥ a_1, (↑M : EReal) < (↑a : EReal) * (↑b : EReal)

Tactic:
refine ⟨n + 1, fun k k_n ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
n : ℕ
hn : M / a ≤ (↑n : ℝ)
k : ℕ
k_n : k ≥ n + 1
rw : M < (↑k : ℝ) * a
⊢ (↑M : EReal) < (↑a : EReal) * (↑k : EReal)

Tactic:
rw [← coe_coe_eq_natCast, ← coe_mul, EReal.coe_lt_coe_iff, mul_comm]

Premises used: EReal.coe_coe_eq_natCast, mul_comm, EReal.coe_mul, EReal.coe_lt_coe_iff
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
n : ℕ
hn : M / a ≤ (↑n : ℝ)
k : ℕ
k_n : k ≥ n + 1
⊢ M < (↑k : ℝ) * a

Tactic:
(div_lt_iff₀ a_0).1 (hn.trans_lt (Nat.cast_lt.2 k_n))

Premises used: Iff.mpr, div_lt_iff₀, Iff.mp, Nat.cast_lt, LE.le.trans_lt
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
h : 0 < linearGrowthInf u
M a : ℝ
a_0 : 0 < a
a_v : (↑a : EReal) < linearGrowthInf u
n : ℕ
hn : M / a ≤ (↑n : ℝ)
k : ℕ
k_n : k ≥ n + 1
⊢ M < (↑k : ℝ) * a

Tactic:
exact (div_lt_iff₀ a_0).1 (hn.trans_lt (Nat.cast_lt.2 k_n))

Premises used: Iff.mpr, div_lt_iff₀, Iff.mp, Nat.cast_lt, LE.le.trans_lt
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
⊢ linearGrowthInf u + linearGrowthInf v ≤ linearGrowthInf (u + v)

Tactic:
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, LinearGrowth.linearGrowthInf
-- 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)
⊢ linearGrowthInf u + linearGrowthInf v ≤ linearGrowthInf (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.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 + v n) / (↑n : EReal) = (u n + 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
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthSup u + linearGrowthInf v

Tactic:
(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, LinearGrowth.linearGrowthSup, LinearGrowth.linearGrowthInf
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf 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)
⊢ linearGrowthInf (u + v) ≤ linearGrowthSup u + linearGrowthInf 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.LinearGrowth
Goal:
u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf 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 + v n) / (↑n : EReal) = (u n + 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
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
rw : linearGrowthInf (v + u) ≤ linearGrowthSup v + linearGrowthInf u
⊢ linearGrowthInf (u + v) ≤ linearGrowthInf u + linearGrowthSup v

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

Premises used: add_comm, LinearGrowth.linearGrowthSup, LinearGrowth.linearGrowthInf