awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
neg : k ≥ M
neg₁ : ∀ (ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)), a * b * (↑k : EReal) ≤ (u ∘ v) k
⊢ ∃ b_1 ≥ M, a' * (↑b_1 : EReal) ≤ (↑(v b_1) : EReal) → a * b * (↑b_1 : EReal) ≤ (u ∘ v) b_1

Tactic:
refine ⟨k, ?_, fun ak_vk' ↦ ?_⟩
-- 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)
neg :
  ∀ (aM_M' : (↑M : EReal) ≤ a'⁻¹ * (↑M' : EReal)) (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)), k ≥ M
⊢ k ≥ M

Tactic:
rw [mul_comm a', ← le_div_iff_mul_le a_0' a_top', EReal.div_eq_inv_mul] at aM_M'

Premises used: EReal.div_eq_inv_mul, mul_comm, 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
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' : (↑M : EReal) ≤ a'⁻¹ * (↑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)
apply : a'⁻¹ * (↑M' : EReal) ≤ a'⁻¹ * (↑n : EReal)
⊢ k ≥ M

Tactic:
apply Nat.cast_le.1 <| aM_M'.trans <| an_k'.trans' _

Premises used: Iff.mp, Nat.cast_le, LE.le.trans, 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
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' : (↑M : EReal) ≤ a'⁻¹ * (↑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)
ha : 0 ≤ a'⁻¹
⊢ a'⁻¹ * (↑M' : EReal) ≤ a'⁻¹ * (↑n : EReal)

Tactic:
gcongr
-- 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)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
neg : b * (a * (↑k : EReal)) ≤ u (v k)
⊢ a * b * (↑k : EReal) ≤ (u ∘ v) k

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 : ℕ → ℕ
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)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
⊢ (↑n : 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) (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)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
an_k'₁ : (↑n : EReal) ≤ a' * (↑k : EReal)
⊢ (↑k : EReal) ≤ a⁻¹ * (↑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) (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)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
an_k'₁ : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an₁ : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
⊢ a' * (↑k : EReal) ≤ (↑(v 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) (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' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
⊢ a * (↑k : EReal) ≤ (↑n : EReal)

Tactic:
rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0 (ne_top_of_lt a_a'), mul_comm] at k_an

Premises used: EReal.div_eq_inv_mul, mul_comm, ne_top_of_lt, 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
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' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : (↑k : EReal) ≤ a⁻¹ * (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
k_an₁ : a * (↑k : EReal) ≤ (↑n : EReal)
⊢ a' * (↑k : EReal) ≤ (↑(v k) : EReal)

Tactic:
rw [← EReal.div_eq_inv_mul, le_div_iff_mul_le a_0 (ne_top_of_lt a_a'), mul_comm] at k_an

Premises used: EReal.div_eq_inv_mul, mul_comm, ne_top_of_lt, 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
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' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : a * (↑k : EReal) ≤ (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
⊢ n ≤ v k

Tactic:
have n_vk := Nat.cast_le.1 (an_k'.trans ak_vk')
-- 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' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : a * (↑k : EReal) ≤ (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
n_vk : n ≤ v k
ha : 0 ≤ b
⊢ b * (a * (↑k : EReal)) ≤ b * (↑n : EReal)

Tactic:
gcongr
-- 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' : (↑n : EReal) ≤ a' * (↑k : EReal)
k_an : a * (↑k : EReal) ≤ (↑n : EReal)
ak_vk' : a' * (↑k : EReal) ≤ (↑(v k) : EReal)
n_vk : n ≤ v k
⊢ b * (a * (↑k : EReal)) ≤ u (v k)

Tactic:
exact le_trans (by gcongr) <| bn_un.trans (h n_vk)

Premises used: LE.le.trans, le_trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ Ne (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0

Tactic:
rw [← hv.liminf_eq] at ha

Premises used: Filter.Tendsto.liminf_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
ha₁ : Ne (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
⊢ a ≠ ⊤

Tactic:
rw [← hv.liminf_eq] at ha

Premises used: Filter.Tendsto.liminf_eq
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : Ne (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
ha' : a ≠ ⊤
⊢ LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)

Tactic:
ha.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)

Premises used: Ne.symm, LinearGrowth.linearGrowthInf_natCast_nonneg, Ne.lt_of_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : Ne (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0
ha' : a ≠ ⊤
⊢ LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)

Tactic:
exact ha.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)

Premises used: Ne.symm, LinearGrowth.linearGrowthInf_natCast_nonneg, Ne.lt_of_le
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
⊢ LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)

Tactic:
have hv₁ : 0 < liminf (fun n ↦ (v n : EReal) / n) atTop := by
    rw [← hv.liminf_eq] at ha
    exact ha.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
⊢ Tendsto v atTop atTop

Tactic:
have v_top := tendsto_atTop_of_linearGrowthInf_natCast_pos hv₁.ne.symm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
pos : ∀ (u_0 : u = ⊥), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
neg : ∀ (u_0 : ¬u = ⊥), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
by_cases u_0 : u = ⊥
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : u = ⊥
pos : linearGrowthInf (⊥ ∘ v) = a * linearGrowthInf ⊥
pos₁ : linearGrowthInf ⊥ = a * linearGrowthInf ⊥
pos₂ : ⊥ = a * ⊥
pos₃ : ⊥ = HMul.hMul (α := EReal) (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊥
pos₄ pos₅ : Eq (α := EReal) ⊥ ⊥
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
rw [u_0, Pi.bot_comp, linearGrowthInf_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]

Premises used: LinearGrowth.linearGrowthInf_bot, Pi.bot_comp, Filter.Tendsto.liminf_eq, EReal.mul_bot_of_pos
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
pos : ∀ (h' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
neg : ∀ (h' : ∀ᶠ (x : ℕ) in atTop, 0 < u x), linearGrowthInf (u ∘ v) = a * linearGrowthInf u
⊢ linearGrowthInf (u ∘ v) = a * linearGrowthInf u

Tactic:
by_cases! h' : ∃ᶠ n : ℕ in atTop, u n ≤ 0

Premises used: Filter.atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0
n : ℕ
obtain : ∀ (m : ℕ) (n_m : m ≥ n) (um_1 : u m ≤ 0), u n ≤ 0
⊢ u n ≤ 0

Tactic:
obtain ⟨m, n_m, um_1⟩ := (frequently_atTop.1 h') n

Premises used: Filter.frequently_atTop, Iff.mp
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0
n m : ℕ
n_m : m ≥ n
um_1 : u m ≤ 0
⊢ u n ≤ 0

Tactic:
(h n_m).trans um_1

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0
n m : ℕ
n_m : m ≥ n
um_1 : u m ≤ 0
⊢ u n ≤ 0

Tactic:
exact (h n_m).trans um_1

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∃ᶠ (n : ℕ) in atTop, u n ≤ 0
⊢ ∀ (n : ℕ), u n ≤ 0

Tactic:
replace h' (n : ℕ) : u n ≤ 0 := by
      obtain ⟨m, n_m, um_1⟩ := (frequently_atTop.1 h') n
      exact (h n_m).trans um_1
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
apply : linearGrowthInf u ≤ 0
⊢ linearGrowthInf u = 0

Tactic:
apply le_antisymm _ (h.linearGrowthInf_nonneg u_0)

Premises used: Monotone.linearGrowthInf_nonneg, le_antisymm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
⊢ linearGrowthInf u ≤ 0

Tactic:
(linearGrowthInf_monotone h').trans_eq (linearGrowthInf_const zero_ne_bot zero_ne_top)

Premises used: EReal.zero_ne_bot, LE.le.trans_eq, LinearGrowth.linearGrowthInf_const, EReal.zero_ne_top, LinearGrowth.linearGrowthInf_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
⊢ linearGrowthInf u ≤ 0

Tactic:
exact (linearGrowthInf_monotone h').trans_eq (linearGrowthInf_const zero_ne_bot zero_ne_top)

Premises used: EReal.zero_ne_bot, LE.le.trans_eq, LinearGrowth.linearGrowthInf_const, EReal.zero_ne_top, LinearGrowth.linearGrowthInf_monotone
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
v : ℕ → ℕ
a : EReal
h : Monotone u
hv : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop (𝓝 a)
ha : a ≠ 0
ha' : a ≠ ⊤
hv₁ : LT.lt (α := EReal) 0 (liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop)
v_top : Tendsto v atTop atTop
u_0 : ¬u = ⊥
h' : ∀ (n : ℕ), u n ≤ 0
⊢ linearGrowthInf u = 0

Tactic:
have u_0' : linearGrowthInf u = 0 := by
      apply le_antisymm _ (h.linearGrowthInf_nonneg u_0)
      exact (linearGrowthInf_monotone h').trans_eq (linearGrowthInf_const zero_ne_bot zero_ne_top)