awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthInf v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthInf v
have inr : linearGrowthInf v + 0 = linearGrowthInf v
Tactic: rw [linearGrowthSup_const b_bot.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
have rw : linearGrowthInf v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤
Tactic: rw [linearGrowthSup_const b_bot.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥
have rw : linearGrowthInf v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥
Tactic: rw [linearGrowthSup_const b_bot.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ linearGrowthSup u ≤ linearGrowthSup v
have apply : (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
Tactic: apply (linearGrowthSup_eventually_monotone h).trans
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
have inl : ∀ (hb : Ne (α := EReal) ⊥ ⊤) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥),
  (linearGrowthSup fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthSup v
Tactic: rcases eq_bot_or_bot_lt b with rfl | b_bot
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
inl :
  ∀ (hb : Ne (α := EReal) ⊥ ⊤) (h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + ⊥),
    (linearGrowthSup fun (x : ℕ) ↦ v x + ⊥) ≤ linearGrowthSup v
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
have inr : ∀ (b_bot : ⊥ < b), (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
Tactic: rcases eq_bot_or_bot_lt b with rfl | b_bot
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
have inr : (linearGrowthSup v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthSup v
Tactic: apply (linearGrowthSup_add_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : (linearGrowthSup v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthSup v
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
have apply : linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
Tactic: apply (linearGrowthSup_add_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
inr : (linearGrowthSup v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthSup v
apply : linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
⊢ (linearGrowthSup fun (x : ℕ) ↦ v x + b) ≤ linearGrowthSup v
have apply₁ : linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥
Tactic: apply (linearGrowthSup_add_le _ _).trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ (linearGrowthSup v + linearGrowthSup fun (x : ℕ) ↦ b) = linearGrowthSup v
have inr : linearGrowthSup v + 0 = linearGrowthSup v
Tactic: rw [linearGrowthSup_const b_bot.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊤
have rw : linearGrowthSup v ≠ ⊥ ∨ Ne (α := EReal) 0 ⊤
Tactic: rw [linearGrowthSup_const b_bot.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
b_bot : ⊥ < b
⊢ linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) (linearGrowthSup fun (x : ℕ) ↦ b) ⊥
have rw : linearGrowthSup v ≠ ⊤ ∨ Ne (α := EReal) 0 ⊥
Tactic: rw [linearGrowthSup_const b_bot.ne' hb]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
⊢ linearGrowthInf (u ⊓ v) = min (linearGrowthInf u) (linearGrowthInf v)
have rw : Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (u ⊓ v) n / (↑n : EReal)) atTop)
  (liminf (fun (a : ℕ) ↦ min (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)
Tactic: rw [linearGrowthInf, linearGrowthInf, linearGrowthInf, ← liminf_min]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
⊢ Eq (α := EReal) (liminf (fun (n : ℕ) ↦ (u ⊓ v) n / (↑n : EReal)) atTop)
    (liminf (fun (a : ℕ) ↦ min (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)
have refine : ∀ (n : ℕ), (u ⊓ v) n / (↑n : EReal) = min (u n / (↑n : EReal)) (v n / (↑n : EReal))
Tactic: refine liminf_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ Eq (α := EReal) (linearGrowthInf (⨅ x ∈ s, u x)) (⨅ x ∈ s, linearGrowthInf (u x))
have this : Eq (α := EReal) ((linearGrowthInfTopHom : (a : ℕ → EReal) → EReal) (hs.toFinset (s := s).inf u) : EReal)
  (hs.toFinset (s := s).inf ((⇑linearGrowthInfTopHom : (a : ℕ → EReal) → EReal) ∘ u) : EReal)
Tactic: have := map_finset_inf linearGrowthInfTopHom hs.toFinset u
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
⊢ Eq (α := EReal) (linearGrowthInf (⨅ (i : ι), u i)) (⨅ (i : ι), linearGrowthInf (u i))
have rw : Eq (α := EReal) (linearGrowthInf (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
  (⨅ (i : ι), linearGrowthInf (u i))
Tactic: rw [← iInf_univ, linearGrowthInf_biInf u Set.finite_univ, iInf_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
rw :
  Eq (α := EReal) (linearGrowthInf (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
    (⨅ (i : ι), linearGrowthInf (u i))
⊢ Eq (α := EReal) (linearGrowthInf (⨅ (i : ι), u i)) (⨅ (i : ι), linearGrowthInf (u i))
have rw₁ : Eq (α := EReal) (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), linearGrowthInf (u x))
  (⨅ (i : ι), linearGrowthInf (u i))
Tactic: rw [← iInf_univ, linearGrowthInf_biInf u Set.finite_univ, iInf_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
rw :
  Eq (α := EReal) (linearGrowthInf (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
    (⨅ (i : ι), linearGrowthInf (u i))
rw₁ :
  Eq (α := EReal) (⨅ (x : ι), ⨅ (_ : Membership.mem (γ := Set ι) Set.univ x), linearGrowthInf (u x))
    (⨅ (i : ι), linearGrowthInf (u i))
⊢ Eq (α := EReal) (linearGrowthInf (⨅ (i : ι), u i)) (⨅ (i : ι), linearGrowthInf (u i))
have rw₂ : Eq (α := EReal) (⨅ (x : ι), linearGrowthInf (u x)) (⨅ (i : ι), linearGrowthInf (u i))
Tactic: rw [← iInf_univ, linearGrowthInf_biInf u Set.finite_univ, iInf_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
⊢ linearGrowthSup (u ⊔ v) = max (linearGrowthSup u) (linearGrowthSup v)
have rw : Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (u ⊔ v) n / (↑n : EReal)) atTop)
  (limsup (fun (a : ℕ) ↦ max (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)
Tactic: rw [linearGrowthSup, linearGrowthSup, linearGrowthSup, ← limsup_max]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u v : ℕ → EReal
⊢ Eq (α := EReal) (limsup (fun (n : ℕ) ↦ (u ⊔ v) n / (↑n : EReal)) atTop)
    (limsup (fun (a : ℕ) ↦ max (u a / (↑a : EReal)) (v a / (↑a : EReal))) atTop)
have refine : ∀ (n : ℕ), (u ⊔ v) n / (↑n : EReal) = max (u n / (↑n : EReal)) (v n / (↑n : EReal))
Tactic: refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ Eq (α := EReal) (linearGrowthSup (⨆ x ∈ s, u x)) (⨆ x ∈ s, linearGrowthSup (u x))
have this : Eq (α := EReal) ((linearGrowthSupBotHom : (a : ℕ → EReal) → EReal) (hs.toFinset (s := s).sup u) : EReal)
  (hs.toFinset (s := s).sup ((⇑linearGrowthSupBotHom : (a : ℕ → EReal) → EReal) ∘ u) : EReal)
Tactic: have := map_finset_sup linearGrowthSupBotHom hs.toFinset u
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
⊢ Eq (α := EReal) (linearGrowthSup (⨆ (i : ι), u i)) (⨆ (i : ι), linearGrowthSup (u i))
have rw : Eq (α := EReal) (linearGrowthSup (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
  (⨆ (i : ι), linearGrowthSup (u i))
Tactic: rw [← iSup_univ, linearGrowthSup_biSup u Set.finite_univ, iSup_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
rw :
  Eq (α := EReal) (linearGrowthSup (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
    (⨆ (i : ι), linearGrowthSup (u i))
⊢ Eq (α := EReal) (linearGrowthSup (⨆ (i : ι), u i)) (⨆ (i : ι), linearGrowthSup (u i))
have rw₁ : Eq (α := EReal) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), linearGrowthSup (u x))
  (⨆ (i : ι), linearGrowthSup (u i))
Tactic: rw [← iSup_univ, linearGrowthSup_biSup u Set.finite_univ, iSup_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
ι : Type u_1
inst : Finite ι
u : ι → ℕ → EReal
rw :
  Eq (α := EReal) (linearGrowthSup (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), u x))
    (⨆ (i : ι), linearGrowthSup (u i))
rw₁ :
  Eq (α := EReal) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) Set.univ x), linearGrowthSup (u x))
    (⨆ (i : ι), linearGrowthSup (u i))
⊢ Eq (α := EReal) (linearGrowthSup (⨆ (i : ι), u i)) (⨆ (i : ι), linearGrowthSup (u i))
have rw₂ : Eq (α := EReal) (⨆ (x : ι), linearGrowthSup (u x)) (⨆ (i : ι), linearGrowthSup (u i))
Tactic: rw [← iSup_univ, linearGrowthSup_biSup u Set.finite_univ, iSup_univ]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a b : ℝ
h : a < b
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
have refine : ∀ (x : ℝ) (ab_x : (b - a)⁻¹ ≤ x), ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
Tactic: refine (eventually_ge_atTop (b - a)⁻¹).mono fun x ab_x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
a b : ℝ
h : a < b
x : ℝ
ab_x : (b - a)⁻¹ ≤ x
⊢ ∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
have ab_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
Cleared hypotheses: ab_x
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
x : ℝ
x_0 : 0 ≤ x
⊢ (∃ (n : ℤ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x) → ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
have h₁ : ∀ (m : ℤ) (m_a : a * x ≤ (↑m : ℝ)) (m_b : (↑m : ℝ) ≤ b * x), ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
Tactic: ⟨m, m_a, m_b⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a b : ℝ
h : a < b
hb : 0 ≤ b
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ (n : ℕ), a * x ≤ (↑n : ℝ) ∧ (↑n : ℝ) ≤ b * x
have h₁ : ∀ (x : ℝ) (x_0 : 0 ≤ x) (m : ℤ) (m_a : a * x ≤ (↑m : ℝ)) (m_b : (↑m : ℝ) ≤ b * x),
  ∃ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
have h₁ : (↑m.toNat : ℝ) ≤ b * x
Tactic: refine ⟨m.toNat, m_a.trans (Int.cast_le.2 m.self_le_toNat), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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
⊢ (↑m.toNat : ℝ) ≤ b * x
have apply : Eq (α := ℝ) (↑m.toNat : ℝ) (max (↑m : ℝ) 0)
Tactic: apply le_of_eq_of_le _ (max_le m_b (mul_nonneg hb x_0))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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)
have refine_1 : ∀ (n : ℕ), HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑0 : EReal)
Tactic: refine Eventually.of_forall fun n ↦ ⟨0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
refine_1 : ∀ (n : ℕ), HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑0 : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop, ∃ (m : ℕ), HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ b * (↑n : EReal)
have refine_2 : ∀ (n : ℕ), (↑0 : EReal) ≤ b * (↑n : EReal)
Tactic: refine Eventually.of_forall fun n ↦ ⟨0, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ (↑0 : EReal)
have refine_1 : HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ 0
Tactic: rw [Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ (↑0 : EReal) ≤ b * (↑n : EReal)
have refine_2 : 0 ≤ b * (↑n : EReal)
Tactic: rw [Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a b : EReal
hb : 0 ≤ b
h : ⊥ < b
n : ℕ
⊢ HMul.hMul (α := EReal) ⊥ (↑n : EReal) ≤ 0
have refine_1 : LE.le (α := EReal) 0 ⊥ ∧ LE.le (α := EReal) (↑n : EReal) 0 ∨ LE.le (α := EReal) ⊥ 0 ∧ LE.le (α := EReal) 0 (↑n : EReal)
Tactic: apply mul_nonpos_iff.2
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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)
have refine : ∀ (n : ℕ) (n_0 : 0 < n),
  ∃ (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 ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a_1 b : EReal
a : ℝ
hb : LE.le (α := EReal) 0 ⊤
h : (↑a : EReal) < ⊤
n : ℕ
n_0 : 0 < n
⊢ ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ HMul.hMul (α := EReal) ⊤ (↑n : EReal)
have obtain : ∀ (m : ℕ) (hm : (↑a : EReal) * (↑n : EReal) ≤ (↑m : 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
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
a_1 b_1 : EReal
a b : ℝ
hb : 0 ≤ (↑b : EReal)
h : (↑a : EReal) < (↑b : EReal)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)
have 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)
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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : ℕ) in atTop,
    ∃ (m : ℕ), (↑a : EReal) * (↑n : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑n : EReal)
have obtain : ∀ (n : ℕ) (x_n : x ≤ (↑n : ℝ)),
  ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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)
have refine : ∀ (k : ℕ) (n_k : k ≥ n),
  ∃ (m : ℕ), (↑a : EReal) * (↑k : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑k : EReal)
Tactic: refine eventually_atTop.2 ⟨n, fun k n_k ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : EReal) * (↑k : EReal) ≤ (↑m : EReal) ∧ (↑m : EReal) ≤ (↑b : EReal) * (↑k : EReal)
have simp : ∃ (m : ℕ), a * (↑k : ℝ) ≤ (↑m : ℝ) ∧ (↑m : ℝ) ≤ b * (↑k : ℝ)
Tactic: simp only [← coe_coe_eq_natCast, ← EReal.coe_mul, EReal.coe_le_coe_iff]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
v : ℕ → ℕ
h : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
⊢ Tendsto v atTop atTop
have refine : ∀ (M : ℕ), ∀ᶠ (a : ℕ) in atTop, M ≤ v a
Tactic: refine tendsto_atTop.2 fun M ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
v : ℕ → ℕ
h : Ne (α := EReal) (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) 0
M : ℕ
⊢ ∀ᶠ (a : ℕ) in atTop, M ≤ v a
have this : Tendsto (β := EReal) (fun (n : ℕ) ↦ (↑(v n) : EReal)) atTop (𝓝 ⊤)
Tactic: have := tendsto_atTop_of_linearGrowthInf_pos (h.lt_of_le' (linearGrowthInf_natCast_nonneg v))
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ 0 ≤ linearGrowthInf (u ∘ v)
have rw : (linearGrowthInf fun (x : ℕ) ↦ 0) ≤ linearGrowthInf (u ∘ v)
Tactic: rw [← linearGrowthInf_const zero_ne_bot zero_ne_top]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)
have uv_0 : 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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
⊢ (linearGrowthInf fun (n : ℕ) ↦ (↑(v n) : EReal)) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)
have 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)
Tactic: apply EReal.mul_le_of_forall_lt_of_nonneg (linearGrowthInf_natCast_nonneg v) uv_0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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)
have 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
Tactic: refine fun a ⟨_, a_v⟩ b ⟨b_0, b_u⟩ ↦ Eventually.le_linearGrowthInf ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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
⊢ ∀ᶠ (n : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have b_uv : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 : ℕ) in atTop, a * b * (↑n : EReal) ≤ (u ∘ v) n
have 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
Tactic: filter_upwards [b_uv, eventually_lt_of_lt_liminf a_v, eventually_gt_atTop 0]
    with n b_uvn a_vn n_0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
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 * b * (↑n : EReal) ≤ (u ∘ v) n
have a_vn₁ : 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
Cleared hypotheses: a_vn
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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)
⊢ a * b * (↑n : EReal) ≤ (u ∘ v) n
have h : b * (a * (↑n : EReal)) ≤ u (v n)
Tactic: rw [comp_apply, mul_comm a b, mul_assoc b a]