awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
an_k₁ : (↑n : EReal) ≤ a * (↑k : EReal)
⊢ a' * (↑k : EReal) ≤ (↑n : EReal)

Tactic:
rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0 a_top] at an_k

Premises used: EReal.div_eq_inv_mul, EReal.div_le_iff_le_mul
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : a⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
an_k₁ : (↑n : EReal) ≤ a * (↑k : EReal)
k_an'₁ : a' * (↑k : EReal) ≤ (↑n : EReal)
⊢ (↑(v k) : EReal) ≤ a' * (↑k : EReal)

Tactic:
rw [← EReal.div_eq_inv_mul, div_le_iff_le_mul a_0 a_top] at an_k

Premises used: EReal.div_eq_inv_mul, EReal.div_le_iff_le_mul
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : (↑n : EReal) ≤ a * (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
⊢ v k ≤ n

Tactic:
have vk_n := Nat.cast_le.1 (vk_ak'.trans k_an')
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : (↑n : EReal) ≤ a * (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
vk_n : v k ≤ n
ha : 0 ≤ b
⊢ b * (↑n : EReal) ≤ b * (a * (↑k : EReal))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
hv₁ : Ne (α := EReal) (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)) ⊤
u_0 : ¬u = ⊥
v_0 : LT.lt (α := EReal) 0 (linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal))
a : EReal
v_a : a > linearGrowthSup fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, (↑(v n) : EReal) ≤ a' * (↑n : EReal)
u_b :
  ∃ᶠ (x : ℕ) in atTop,
    (u x ≤ b * (↑x : EReal) ∧ 0 < x) ∧ ∃ (m : ℕ), a⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a'⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
un_bn : u n ≤ b * (↑n : EReal)
right : 0 < n
k : ℕ
an_k : (↑n : EReal) ≤ a * (↑k : EReal)
k_an' : a' * (↑k : EReal) ≤ (↑n : EReal)
vk_ak' : (↑(v k) : EReal) ≤ a' * (↑k : EReal)
vk_n : v k ≤ n
⊢ u (v k) ≤ b * (a * (↑k : EReal))

Tactic:
exact (h vk_n).trans <| un_bn.trans <| by gcongr

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
⊢ LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))

Tactic:
have v_0 := hv.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
pos : ∀ (u_0 : u = ⊥), (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
neg : ∀ (u_0 : ¬u = ⊥), (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)

Tactic:
by_cases u_0 : u = ⊥
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : u = ⊥
pos : LE.le (α := EReal) ⊥ (linearGrowthSup (⊥ ∘ v))
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)

Tactic:
rw [u_0, linearGrowthSup_bot, mul_bot_of_pos v_0]

Premises used: LinearGrowth.linearGrowthSup_bot, EReal.mul_bot_of_pos
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : u = ⊥
⊢ LE.le (α := EReal) ⊥ (linearGrowthSup (⊥ ∘ v))

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : u = ⊥
⊢ LE.le (α := EReal) ⊥ (linearGrowthSup (⊥ ∘ v))

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
neg :
  ∀ (a' : EReal),
    Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a' →
      ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a' * b' ≤ linearGrowthSup (u ∘ v)
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)

Tactic:
apply EReal.mul_le_of_forall_lt_of_nonneg v_0.le
    (linearGrowthSup_comp_nonneg h u_0 (tendsto_atTop_of_linearGrowthInf_natCast_pos hv))

Premises used: EReal.mul_le_of_forall_lt_of_nonneg, LT.lt.le, LinearGrowth.tendsto_atTop_of_linearGrowthInf_natCast_pos, LinearGrowth.linearGrowthSup_comp_nonneg
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
neg :
  ∀ (a_0 : 0 < a) (a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)),
    ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a * b' ≤ linearGrowthSup (u ∘ v)
⊢ Membership.mem (γ := Set EReal) (Set.Ioo 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))) a →
    ∀ b' ∈ Set.Ioo 0 (linearGrowthSup u), a * b' ≤ linearGrowthSup (u ∘ v)

Tactic:
⟨a_0, a_v⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
neg : ∀ (b_0 : 0 < b) (b_u : b < linearGrowthSup u), a * b ≤ linearGrowthSup (u ∘ v)
⊢ b ∈ Set.Ioo 0 (linearGrowthSup u) → a * b ≤ linearGrowthSup (u ∘ v)

Tactic:
⟨b_0, b_u⟩
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
neg : ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
⊢ a * b ≤ linearGrowthSup (u ∘ v)

Tactic:
apply Frequently.le_linearGrowthSup

Premises used: Frequently.le_linearGrowthSup
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
neg :
  ∀ (a' : EReal) (a_a' : a < a') (a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)),
    ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n

Tactic:
obtain ⟨a', a_a', a_v'⟩ := exists_between a_v

Premises used: exists_between
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
⊢ a' ≠ ⊤

Tactic:
have a_top' := ne_top_of_lt a_v'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
⊢ 0 < a'

Tactic:
have a_0' := a_0.trans a_a'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
⊢ a'⁻¹ < a⁻¹

Tactic:
have a_a_inv' : a'⁻¹ < a⁻¹ := inv_strictAntiOn (Set.mem_Ioi.2 a_0) (Set.mem_Ioi.2 a_0') a_a'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
h₁ :
  ∀ (n : ℕ) (a_vn' : a' < HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) (n_0 : 0 < n),
    a' * (↑n : EReal) ≤ (↑(v n) : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)

Tactic:
filter_upwards [eventually_lt_of_lt_liminf a_v', eventually_gt_atTop 0] with n 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 : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
n : ℕ
a_vn' : a' < HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)
n_0 : 0 < n
⊢ a' * (↑n : EReal) ≤ (↑(v n) : EReal)

Tactic:
(le_div_iff_mul_le (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn'.le

Premises used: Iff.mpr, LT.lt.le, Iff.mp, EReal.natCast_ne_top, Nat.cast_pos', EReal.le_div_iff_mul_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
n : ℕ
a_vn' : a' < HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)
n_0 : 0 < n
⊢ a' * (↑n : EReal) ≤ (↑(v n) : EReal)

Tactic:
exact (le_div_iff_mul_le (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn'.le

Premises used: Iff.mpr, LT.lt.le, Iff.mp, EReal.natCast_ne_top, Nat.cast_pos', EReal.le_div_iff_mul_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_v' : a' < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
⊢ ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)

Tactic:
replace a_v' : ∀ᶠ n : ℕ in atTop, a' * n ≤ v n := by
    filter_upwards [eventually_lt_of_lt_liminf a_v', eventually_gt_atTop 0] with n a_vn' n_0
    exact (le_div_iff_mul_le (Nat.cast_pos'.2 n_0) (natCast_ne_top n)).1 a_vn'.le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
neg :
  (∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)) → ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
⊢ ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n

Tactic:
suffices h : (∀ᶠ n : ℕ in atTop, a' * n ≤ v n) → ∃ᶠ n : ℕ in atTop, a * b * n ≤ (u ∘ v) n
    from h a_v'
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
neg : ∃ᶠ (x : ℕ) in atTop, a' * (↑x : EReal) ≤ (↑(v x) : EReal) → a * b * (↑x : EReal) ≤ (u ∘ v) x
⊢ (∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)) → ∃ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n

Tactic:
rw [← frequently_imp_distrib]

Premises used: Filter.frequently_imp_distrib
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
b_u : b < linearGrowthSup u
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
⊢ ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)

Tactic:
replace b_u := ((frequently_mul_le b_u).and_eventually (eventually_gt_atTop 0)).and_eventually
    <| EReal.eventually_atTop_exists_nat_between a_a_inv' (inv_nonneg_of_nonneg a_0.le)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
⊢ ∃ᶠ (x : ℕ) in atTop, a' * (↑x : EReal) ≤ (↑(v x) : EReal) → a * b * (↑x : EReal) ≤ (u ∘ v) x

Tactic:
frequently_atTop.2 fun M ↦ ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
neg : ∀ (M : ℕ), ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
⊢ ∃ᶠ (x : ℕ) in atTop, a' * (↑x : EReal) ≤ (↑(v x) : EReal) → a * b * (↑x : EReal) ≤ (u ∘ v) x

Tactic:
refine frequently_atTop.2 fun M ↦ ?_

Premises used: Iff.mpr, Filter.frequently_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M : ℕ
neg :
  ∀ (M' : ℕ) (aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)),
    ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1

Tactic:
obtain ⟨M', aM_M'⟩ := exists_nat_ge_mul a_top' M

Premises used: EReal.exists_nat_ge_mul
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
neg :
  ∀ (n : ℕ) (n_M' : n ≥ M') (bn_un : b * (↑n : EReal) ≤ u n),
    0 < n →
      ∀ (k : ℕ) (an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)) (k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)),
        ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1

Tactic:
obtain ⟨n, n_M', ⟨bn_un, _⟩, k, an_k', k_an⟩ := frequently_atTop.1 b_u M'

Premises used: Filter.frequently_atTop, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
v_0 : LT.lt (α := EReal) 0 (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal))
u_0 : ¬u = ⊥
a : EReal
a_0 : 0 < a
a_v : a < linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)
b : EReal
b_0 : 0 < b
a' : EReal
a_a' : a < a'
a_top' : a' ≠ ⊤
a_0' : 0 < a'
a_a_inv' : a'⁻¹ < a⁻¹
a_v' : ∀ᶠ (n : ℕ) in atTop, a' * (↑n : EReal) ≤ (↑(v n) : EReal)
b_u :
  ∃ᶠ (x : ℕ) in atTop,
    (b * (↑x : EReal) ≤ u x ∧ 0 < x) ∧ ∃ (m : ℕ), a'⁻¹ * (↑x : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ a⁻¹ * (↑x : EReal)
M M' : ℕ
aM_M' : a' * (↑M : EReal) ≤ (↑M' : EReal)
n : ℕ
n_M' : n ≥ M'
bn_un : b * (↑n : EReal) ≤ u n
right : 0 < n
k : ℕ
an_k' : a'⁻¹ * (↑n : EReal) ≤ (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1

Tactic:
⟨k, ?_, fun ak_vk' ↦ ?_⟩

Premises used: And.intro, Exists.intro