awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
refine : ∀ (x : ℝ) (ab_x : (b - a)⁻¹ ≤ x), ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

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

Premises used: HSub.hSub, Filter.Eventually.mono, Inv.inv, Filter.eventually_ge_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
x : ℝ
ab_x : (b - a)⁻¹ ≤ x
⊢ a * x + 1 ≤ b * x

Tactic:
rw [inv_le_iff_one_le_mul₀ (sub_pos_of_lt h), mul_comm, sub_mul, le_sub_iff_add_le'] at ab_x

Premises used: le_sub_iff_add_le', sub_mul, inv_le_iff_one_le_mul₀, mul_comm, sub_pos_of_lt
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
x : ℝ
ab_x : a * x + 1 ≤ b * x
⊢ ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

Tactic:
⟨_, le_of_add_le_add_right (ab_x.trans (Int.lt_floor_add_one _).le), Int.floor_le _⟩

Premises used: le_of_add_le_add_right, Int.lt_floor_add_one, LT.lt.le, And.intro, Exists.intro, Int.floor_le, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
x : ℝ
ab_x : a * x + 1 ≤ b * x
⊢ ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

Tactic:
exact ⟨_, le_of_add_le_add_right (ab_x.trans (Int.lt_floor_add_one _).le), Int.floor_le _⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
x : ℝ
x_0 : 0 ≤ x
h₁ : ∀ (m : ℤ) (m_a : a * x ≤ (↑m : ℝ)) (m_b : (↑m : ℝ) ≤ b * x), ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
⊢ (∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x) → ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

Tactic:
⟨m, m_a, m_b⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
h₁ :
  ∀ (x : ℝ) (x_0 : 0 ≤ x) (m : ℤ) (m_a : a * x ≤ (↑m : ℝ)) (m_b : (↑m : ℝ) ≤ b * x),
    ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

Tactic:
filter_upwards [eventually_ge_atTop 0, Real.eventually_atTop_exists_int_between h]
    with x x_0 ⟨m, m_a, m_b⟩

Premises used: LinearGrowth.Real.eventually_atTop_exists_int_between, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
x : ℝ
x_0 : 0 ≤ x
m : ℤ
m_a : a * x ≤ (↑m : ℝ)
m_b : (↑m : ℝ) ≤ b * x
⊢ ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

Tactic:
⟨m.toNat, m_a.trans (Int.cast_le.2 m.self_le_toNat), ?_⟩

Premises used: Iff.mpr, Int.self_le_toNat, Int.cast_le, And.intro, Exists.intro, Int.toNat, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
x : ℝ
x_0 : 0 ≤ x
m : ℤ
m_a : a * x ≤ (↑m : ℝ)
m_b : (↑m : ℝ) ≤ b * x
h₁ : (↑m.toNat : ℝ) ≤ b * x
⊢ ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x

Tactic:
refine ⟨m.toNat, m_a.trans (Int.cast_le.2 m.self_le_toNat), ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
x : ℝ
x_0 : 0 ≤ x
m : ℤ
m_a : a * x ≤ (↑m : ℝ)
m_b : (↑m : ℝ) ≤ b * x
apply : Eq (α := ℝ) (↑m.toNat : ℝ) (max (↑m : ℝ) 0)
⊢ (↑m.toNat : ℝ) ≤ b * x

Tactic:
apply le_of_eq_of_le _ (max_le m_b (mul_nonneg hb x_0))

Premises used: mul_nonneg, max_le, le_of_eq_of_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
x : ℝ
x_0 : 0 ≤ x
m : ℤ
m_a : a * x ≤ (↑m : ℝ)
m_b : (↑m : ℝ) ≤ b * x
⊢ Eq (α := ℝ) (↑m.toNat : ℝ) (max (↑m : ℝ) 0)

Tactic:
exact_mod_cast Int.toNat_eq_max m

Premises used: Int.toNat_eq_max
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
⊢ ∀ᶠ (n : ℕ) in atTop, ∃ (m : ℕ), HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ b * (↑n : EReal)

Tactic:
Eventually.of_forall fun n ↦ ⟨0, ?_, ?_⟩

Premises used: Filter.Eventually.of_forall, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
refine_1 : ∀ (n : ℕ), HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑0 : EReal)
refine_2 : ∀ (n : ℕ), (↑0 : EReal) ≤ b * (↑n : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop, ∃ (m : ℕ), HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ b * (↑n : EReal)

Tactic:
refine Eventually.of_forall fun n ↦ ⟨0, ?_, ?_⟩

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
refine_1 : HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ 0
⊢ HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑0 : EReal)

Tactic:
rw [Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
refine_2 : 0 ≤ b * (↑n : EReal)
⊢ (↑0 : EReal) ≤ b * (↑n : EReal)

Tactic:
rw [Nat.cast_zero]

Premises used: Nat.cast_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
refine_1 :
  LE.le (α := EReal) 0 ⊥ ∧ LE.le (α := EReal) (↑n : EReal) 0 ∨
    LE.le (α := EReal) ⊥ 0 ∧ LE.le (α := EReal) 0 (↑n : EReal)
⊢ HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ 0

Tactic:
apply mul_nonpos_iff.2

Premises used: Iff.mpr, EReal.mul_nonpos_iff
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ LE.le (α := EReal) 0 ⊥ ∧ LE.le (α := EReal) (↑n : EReal) 0 ∨
    LE.le (α := EReal) ⊥ 0 ∧ LE.le (α := EReal) 0 (↑n : EReal)

Tactic:
.inr ⟨bot_le, n.cast_nonneg'⟩

Premises used: Nat.cast_nonneg', And.intro, bot_le, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ LE.le (α := EReal) 0 ⊥ ∧ LE.le (α := EReal) (↑n : EReal) 0 ∨
    LE.le (α := EReal) ⊥ 0 ∧ LE.le (α := EReal) 0 (↑n : EReal)

Tactic:
exact .inr ⟨bot_le, n.cast_nonneg'⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ 0 ≤ b * (↑n : EReal)

Tactic:
positivity
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b : EReal
a : ℝ
hb : LE.le (α := EReal) 0 ⊤
h : (↑a : EReal) < ⊤
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)

Tactic:
(eventually_gt_atTop 0).mono fun n n_0 ↦ ?_

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b : EReal
a : ℝ
hb : LE.le (α := EReal) 0 ⊤
h : (↑a : EReal) < ⊤
refine :
  ∀ (n : ℕ) (n_0 : 0 < n),
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)

Tactic:
refine (eventually_gt_atTop 0).mono fun n n_0 ↦ ?_

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b : EReal
a : ℝ
hb : LE.le (α := EReal) 0 ⊤
h : (↑a : EReal) < ⊤
n : ℕ
n_0 : 0 < n
obtain :
  ∀ (m : ℕ) (hm : (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)),
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)

Tactic:
obtain ⟨m, hm⟩ := exists_nat_ge_mul h.ne n

Premises used: EReal.exists_nat_ge_mul, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b : EReal
a : ℝ
hb : LE.le (α := EReal) 0 ⊤
h : (↑a : EReal) < ⊤
n : ℕ
n_0 : 0 < n
m : ℕ
hm : (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)

Tactic:
⟨m, hm, le_of_le_of_eq le_top (top_mul_of_pos (Nat.cast_pos'.2 n_0)).symm⟩

Premises used: Iff.mpr, le_of_le_of_eq, EReal.top_mul_of_pos, le_top, And.intro, Exists.intro, Eq.symm, Nat.cast_pos'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b : EReal
a : ℝ
hb : LE.le (α := EReal) 0 ⊤
h : (↑a : EReal) < ⊤
n : ℕ
n_0 : 0 < n
m : ℕ
hm : (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal)
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)

Tactic:
exact ⟨m, hm, le_of_le_of_eq le_top (top_mul_of_pos (Nat.cast_pos'.2 n_0)).symm⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
obtain :
  ∀ (x : ℝ) (hx : ∀ b_2 ≥ x, ∃ (n : ℕ), a * b_2 ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * b_2),
    ∀ᶠ (n : ℕ) in atTop,
      ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)

Tactic:
obtain ⟨x, hx⟩ := eventually_atTop.1 <| Real.eventually_atTop_exists_nat_between
        (EReal.coe_lt_coe_iff.1 h) (EReal.coe_nonneg.1 hb)

Premises used: LinearGrowth.Real.eventually_atTop_exists_nat_between, EReal.coe_nonneg, Iff.mp, Filter.eventually_atTop, EReal.coe_lt_coe_iff
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
x : ℝ
hx : ∀ b_2 ≥ x, ∃ (n : ℕ), a * b_2 ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * b_2
obtain :
  ∀ (n : ℕ) (x_n : x ≤ (↑n : ℝ)),
    ∀ᶠ (n : ℕ) in atTop,
      ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)

Tactic:
obtain ⟨n, x_n⟩ := exists_nat_ge x

Premises used: exists_nat_ge
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
x : ℝ
hx : ∀ b_2 ≥ x, ∃ (n : ℕ), a * b_2 ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * b_2
n : ℕ
x_n : x ≤ (↑n : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)

Tactic:
eventually_atTop.2 ⟨n, fun k n_k ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
x : ℝ
hx : ∀ b_2 ≥ x, ∃ (n : ℕ), a * b_2 ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * b_2
n : ℕ
x_n : x ≤ (↑n : ℝ)
refine :
  ∀ (k : ℕ) (n_k : k ≥ n),
    ∃ (m : ℕ), (↑a : EReal) * (↑k : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑k : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)

Tactic:
refine eventually_atTop.2 ⟨n, fun k n_k ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
x : ℝ
hx : ∀ b_2 ≥ x, ∃ (n : ℕ), a * b_2 ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * b_2
n : ℕ
x_n : x ≤ (↑n : ℝ)
k : ℕ
n_k : k ≥ n
simp : ∃ (m : ℕ), a * (↑k : ℝ) ≤ (↑m : ℝ) ∧ (↑m : ℝ) ≤ b * (↑k : ℝ)
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑k : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑k : EReal)

Tactic:
simp only [← coe_coe_eq_natCast, ← EReal.coe_mul, EReal.coe_le_coe_iff]

Premises used: EReal.coe_le_coe_iff, EReal.coe_coe_eq_natCast, EReal.coe_mul
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
x : ℝ
hx : ∀ b_2 ≥ x, ∃ (n : ℕ), a * b_2 ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * b_2
n : ℕ
x_n : x ≤ (↑n : ℝ)
k : ℕ
n_k : k ≥ n
⊢ ∃ (m : ℕ), a * (↑k : ℝ) ≤ (↑m : ℝ) ∧ (↑m : ℝ) ≤ b * (↑k : ℝ)

Tactic:
hx k (x_n.trans (Nat.cast_le.2 n_k))

Premises used: Iff.mpr, Nat.cast, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
x : ℝ
hx : ∀ b_2 ≥ x, ∃ (n : ℕ), a * b_2 ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * b_2
n : ℕ
x_n : x ≤ (↑n : ℝ)
k : ℕ
n_k : k ≥ n
⊢ ∃ (m : ℕ), a * (↑k : ℝ) ≤ (↑m : ℝ) ∧ (↑m : ℝ) ≤ b * (↑k : ℝ)

Tactic:
exact hx k (x_n.trans (Nat.cast_le.2 n_k))

Premises used: Iff.mpr, Nat.cast, Nat.cast_le, LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
v : ℕ → ℕ
h : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
⊢ Tendsto v atTop atTop

Tactic:
tendsto_atTop.2 fun M ↦ ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
v : ℕ → ℕ
h : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
refine : ∀ (M : ℕ), ∀ᶠ (a : ℕ) in atTop, M ≤ v a
⊢ Tendsto v atTop atTop

Tactic:
refine tendsto_atTop.2 fun M ↦ ?_

Premises used: Iff.mpr, Filter.tendsto_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
v : ℕ → ℕ
h : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
M : ℕ
⊢ Tendsto (β := EReal) (fun (n : ℕ) ↦ (↑(v n) : EReal)) atTop (𝓝 ⊤)

Tactic:
have := tendsto_atTop_of_linearGrowthInf_pos (h.lt_of_le' (linearGrowthInf_natCast_nonneg v))
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
v : ℕ → ℕ
h : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
M : ℕ
this : Tendsto (β := EReal) (fun (n : ℕ) ↦ (↑(v n) : EReal)) atTop (𝓝 ⊤)
n : ℕ
⊢ (↑(↑M : ℝ) : EReal) < (↑(v n) : EReal) → M ≤ v n

Tactic:
exact_mod_cast le_of_lt

Premises used: le_of_lt
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
v : ℕ → ℕ
h : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
M : ℕ
this : Tendsto (β := EReal) (fun (n : ℕ) ↦ (↑(v n) : EReal)) atTop (𝓝 ⊤)
⊢ ∀ᶠ (a : ℕ) in atTop, M ≤ v a

Tactic:
exact (tendsto_nhds_top_iff_real.1 this M).mono fun n ↦ by exact_mod_cast le_of_lt

Premises used: Nat.cast, Filter.Eventually.mono, EReal.tendsto_nhds_top_iff_real, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
rw : (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ linearGrowthInf (u ∘ v)
⊢ 0 ≤ linearGrowthInf (u ∘ v)

Tactic:
rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]

Premises used: EReal.zero_ne_bot, LinearGrowth.linearGrowthInf_const, EReal.zero_ne_top
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ linearGrowthInf (u ∘ v)

Tactic:
linearGrowthInf_eventually_monotone (hv.eventually hu)

Premises used: LinearGrowth.linearGrowthInf_eventually_monotone, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ linearGrowthInf (u ∘ v)

Tactic:
exact linearGrowthInf_eventually_monotone (hv.eventually hu)

Premises used: LinearGrowth.linearGrowthInf_eventually_monotone, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ 0 ≤ linearGrowthInf (u ∘ v)

Tactic:
have uv_0 : 0 ≤ linearGrowthInf (u ∘ v) := by
    rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]
    exact linearGrowthInf_eventually_monotone (hv.eventually hu)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
apply :
  ∀ (a' : EReal),
    Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a' →
      ∀ b' ∈ Set.Ioo 0 (linearGrowthInf u), a' * b' ≤ linearGrowthInf (u ∘ v)
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)

Tactic:
apply EReal.mul_le_of_forall_lt_of_nonneg (linearGrowthInf_natCast_nonneg v) uv_0

Premises used: EReal.mul_le_of_forall_lt_of_nonneg, LinearGrowth.linearGrowthInf_natCast_nonneg
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
⊢ ∀ (a' : EReal),
    Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a' →
      ∀ b' ∈ Set.Ioo 0 (linearGrowthInf u), a' * b' ≤ linearGrowthInf (u ∘ v)

Tactic:
fun a ⟨_, a_v⟩ b ⟨b_0, b_u⟩ ↦ Eventually.le_linearGrowthInf ?_

Premises used: HMul.hMul, Eventually.le_linearGrowthInf, Function.comp, LE.le, LinearGrowth.linearGrowthInf, _private.0.LinearGrowth.le_linearGrowthInf_comp.match_2, _private.0.LinearGrowth.le_linearGrowthInf_comp.match_1
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
refine :
  ∀ (a : EReal),
    Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a →
      ∀ b ∈ Set.Ioo 0 (linearGrowthInf u),
        0 < a →
          ∀ (a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) (b_0 : 0 < b) (b_u : b < linearGrowthInf u),
            ∀ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
⊢ ∀ (a' : EReal),
    Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a' →
      ∀ b' ∈ Set.Ioo 0 (linearGrowthInf u), a' * b' ≤ linearGrowthInf (u ∘ v)

Tactic:
refine fun a ⟨_, a_v⟩ b ⟨b_0, b_u⟩ ↦ Eventually.le_linearGrowthInf ?_
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
h : Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a
b : EReal
h_1 : b ∈ Set.Ioo 0 (linearGrowthInf u)
left : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b_0 : 0 < b
b_u : b < linearGrowthInf u
⊢ ∀ᶠ (a : ℕ) in atTop, b * (↑(v a) : EReal) ≤ u (v a)

Tactic:
have b_uv := eventually_map.1 ((eventually_mul_le b_u).filter_mono hv)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
h_1 : Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a
b : EReal
h_2 : b ∈ Set.Ioo 0 (linearGrowthInf u)
left : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * (↑(v a) : EReal) ≤ u (v a)
h :
  ∀ (n : ℕ) (b_uvn : b * (↑(v n) : EReal) ≤ u (v n)) (a_vn : a < HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal))
    (n_0 : 0 < n), a * b * (↑n : EReal) ≤ (u ∘ v) n
⊢ ∀ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n

Tactic:
filter_upwards [b_uv, eventually_lt_of_lt_liminf a_v, eventually_gt_atTop 0]
    with n b_uvn a_vn n_0

Premises used: Filter.eventually_lt_of_lt_liminf, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
h : Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a
b : EReal
h_1 : b ∈ Set.Ioo 0 (linearGrowthInf u)
left : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * (↑(v a) : EReal) ≤ u (v a)
n : ℕ
b_uvn : b * (↑(v n) : EReal) ≤ u (v n)
a_vn : a < HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)
n_0 : 0 < n
⊢ a * (↑n : EReal) ≤ (↑(v n) : EReal)

Tactic:
replace a_vn := ((lt_div_iff (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn).le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
h_1 : Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a
b : EReal
h_2 : b ∈ Set.Ioo 0 (linearGrowthInf u)
left : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * (↑(v a) : EReal) ≤ u (v a)
n : ℕ
b_uvn : b * (↑(v n) : EReal) ≤ u (v n)
n_0 : 0 < n
a_vn : a * (↑n : EReal) ≤ (↑(v n) : EReal)
h : b * (a * (↑n : EReal)) ≤ u (v n)
⊢ a * b * (↑n : EReal) ≤ (u ∘ v) n

Tactic:
rw [comp_apply, mul_comm a b, mul_assoc b a]

Premises used: mul_assoc, mul_comm, Function.comp_apply
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
h : Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a
b : EReal
h_1 : b ∈ Set.Ioo 0 (linearGrowthInf u)
left : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * (↑(v a) : EReal) ≤ u (v a)
n : ℕ
b_uvn : b * (↑(v n) : EReal) ≤ u (v n)
n_0 : 0 < n
a_vn : a * (↑n : EReal) ≤ (↑(v n) : EReal)
ha : 0 ≤ b
⊢ b * (a * (↑n : EReal)) ≤ b * (↑(v n) : EReal)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
h : Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a
b : EReal
h_1 : b ∈ Set.Ioo 0 (linearGrowthInf u)
left : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * (↑(v a) : EReal) ≤ u (v a)
n : ℕ
b_uvn : b * (↑(v n) : EReal) ≤ u (v n)
n_0 : 0 < n
a_vn : a * (↑n : EReal) ≤ (↑(v n) : EReal)
⊢ b * (a * (↑n : EReal)) ≤ u (v n)

Tactic:
exact b_uvn.trans' <| by gcongr

Premises used: LE.le.trans'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
⊢ LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))

Tactic:
have v_0 := hv₀.symm.lt_of_le <| (linearGrowthInf_natCast_nonneg v).trans (liminf_le_limsup)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
⊢ linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u

Tactic:
le_mul_of_forall_lt (.inl v_0) (.inl hv₁) ?_

Premises used: EReal.le_mul_of_forall_lt, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
refine :
  ∀ a' > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal), ∀ b' > linearGrowthSup u, linearGrowthSup (u ∘ v) ≤ a' * b'
⊢ linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u

Tactic:
refine le_mul_of_forall_lt (.inl v_0) (.inl hv₁) ?_

Premises used: EReal.le_mul_of_forall_lt, Or.inl
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
hv₂ : Tendsto v atTop atTop
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
⊢ ∀ a' > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal), ∀ b' > linearGrowthSup u, linearGrowthSup (u ∘ v) ≤ a' * b'

Tactic:
fun a v_a b u_b ↦ Eventually.linearGrowthSup_le ?_

Premises used: Eventually.linearGrowthSup_le