awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ linearGrowthSup (u ∘ v) ≤ a * linearGrowthSup u
have neg : ∀ (ha : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) 0)
  (ha' : Ne (α := EReal) (limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop) ⊤)
  (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 = ⊥) (u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x),
  linearGrowthSup (u ∘ v) ≤
    limsup (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u
Tactic: rw [← hv.limsup_eq] at ha ha' ⊢
Cleared hypotheses: ha, ha', hv₁, v_top, u_0, u_1
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
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 = ⊥
u_1 : ∃ᶠ (x : ℕ) in atTop, 0 ≤ u x
⊢ a * linearGrowthSup u ≤ linearGrowthSup (u ∘ v)
have neg : liminf (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(v n) : EReal) (↑n : EReal)) atTop * linearGrowthSup u ≤
  linearGrowthSup (u ∘ v)
Tactic: rw [← hv.liminf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))
have refine : ∀ (x : ℕ) (hx : 0 < x), HDiv.hDiv (α := EReal) (↑(m * x) : EReal) (↑x : EReal) = (↑m : EReal)
Tactic: refine tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (goal)
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
x : ℕ
hx : 0 < x
⊢ HDiv.hDiv (α := EReal) (↑(m * x) : EReal) (↑x : EReal) = (↑m : EReal)
have rw : (↑x : EReal) * HDiv.hDiv (α := EReal) (↑m : EReal) (↑x : EReal) = (↑m : EReal)
Tactic: rw [mul_comm, natCast_mul x m, ← mul_div]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ (linearGrowthInf fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * linearGrowthInf u
have this : Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))
Tactic: have : Tendsto (fun n : ℕ ↦ ((m * n : ℕ) : EReal) / n) atTop (𝓝 m) := by
    refine tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)
    rw [mul_comm, natCast_mul x m, ← mul_div]
    exact mul_div_cancel (natCast_ne_bot x) (natCast_ne_top x) (Nat.cast_ne_zero.2 hx.ne.symm)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.LinearGrowth (hypothesis)
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
⊢ (linearGrowthSup fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * linearGrowthSup u
have this : Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))
Tactic: have : Tendsto (fun n : ℕ ↦ ((m * n : ℕ) : EReal) / n) atTop (𝓝 m) := by
    refine tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)
    rw [mul_comm, natCast_mul x m, ← mul_div]
    exact mul_div_cancel (natCast_ne_bot x) (natCast_ne_top x) (Nat.cast_ne_zero.2 hx.ne.symm)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ IsLittleO (F := 𝕜) (𝓝[≠] a) f fun (x : 𝕜) ↦ (x - a)⁻¹
have refine : Tendsto (Function.comp (β := 𝕜) norm fun (x : 𝕜) ↦ (x - a)⁻¹) (𝓝[≠] a) atTop
Tactic: refine (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr ?_)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ Tendsto (Function.comp (β := 𝕜) norm fun (x : 𝕜) ↦ (x - a)⁻¹) (𝓝[≠] a) atTop
have simp : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖x - a‖⁻¹) (𝓝[≠] a) atTop
Tactic: simp only [Function.comp_def, norm_inv]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q
have noc : NormOneClass R
Tactic: have noc : NormOneClass R := NormMulClass.toNormOneClass
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q
have refine : ∀ (c : ℝ) (cpos : 0 < c), ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ q‖
Tactic: refine IsLittleO.of_bound fun c cpos ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
⊢ ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ q‖
have rw : ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ (q - p + p)‖
Tactic: rw [← Nat.sub_add_cancel hpq.le]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
⊢ ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ (q - p + p)‖
have simp_rw : ∃ v ∈ cobounded R, ∀ y ∈ v, ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)
Tactic: simp_rw [pow_add, norm_mul, norm_pow, eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
⊢ ∃ v ∈ cobounded R, ∀ y ∈ v, ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)
have refine_1 : {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} ∈ cobounded R
Tactic: refine ⟨{y | c⁻¹ ≤ ‖y‖ ^ (q - p)}, ?_, fun y my ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
refine_1 : {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} ∈ cobounded R
⊢ ∃ v ∈ cobounded R, ∀ y ∈ v, ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)
have refine_2 : ∀ (y : R) (my : Membership.mem (γ := Set R) {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} y), ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)
Tactic: refine ⟨{y | c⁻¹ ≤ ‖y‖ ^ (q - p)}, ?_, fun y my ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
⊢ {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} ∈ cobounded R
have key : Tendsto (β := ℝ) (fun (x : R) ↦ ‖x‖ ^ (q - p)) (cobounded R) atTop
Tactic: have key : Tendsto (‖·‖ ^ (q - p)) (cobounded R) atTop :=
      (tendsto_pow_atTop (Nat.sub_ne_zero_iff_lt.mpr hpq)).comp tendsto_norm_cobounded_atTop
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
key : Tendsto (β := ℝ) (fun (x : R) ↦ ‖x‖ ^ (q - p)) (cobounded R) atTop
⊢ {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} ∈ cobounded R
have key₁ : ∀ (b : ℝ), ∀ᶠ (a : R) in cobounded R, b ≤ ‖a‖ ^ (q - p)
Tactic: rw [tendsto_atTop] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
y : R
my : Membership.mem (γ := Set R) {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} y
⊢ ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)
have refine_2 : c⁻¹ * ‖y‖ ^ p ≤ ‖y‖ ^ (q - p) * ‖y‖ ^ p
Tactic: rw [← inv_mul_le_iff₀ cpos]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
c : ℝ
cpos : 0 < c
y : R
my : Membership.mem (γ := Set R) {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} y
⊢ c⁻¹ * ‖y‖ ^ p ≤ ‖y‖ ^ (q - p) * ‖y‖ ^ p
have refine_2 : c⁻¹ ≤ ‖y‖ ^ (q - p)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p ≤ q
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q
have inl : ∀ (hpq : p ≤ p), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ p
Tactic: rcases hpq.eq_or_lt with rfl | h
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p ≤ q
inl : ∀ (hpq : p ≤ p), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ p
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q
have inr : ∀ (h : p < q), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q
Tactic: rcases hpq.eq_or_lt with rfl | h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
⊢ EventuallyEq (β := 𝕜) atTop (fun (x : 𝕜) ↦ x ^ p / x ^ q) fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)
have apply : ∀ (x : 𝕜) (hx : 0 < x),
  Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ x ^ p / x ^ q) x) ((fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) x)
Tactic: apply (eventually_gt_atTop (0 : 𝕜)).mono fun x hx => _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
⊢ EventuallyEq (β := 𝕜) atBot (fun (x : 𝕜) ↦ x ^ p / x ^ q) fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)
have apply : ∀ (x : 𝕜) (hx : x < 0),
  Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ x ^ p / x ^ q) x) ((fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) x)
Tactic: apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ p / x ^ q) atTop atTop
have rw : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop atTop
Tactic: rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop atTop
have hn : 0 < HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)
Tactic: apply tendsto_zpow_atTop_atTop
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ p / x ^ q) atTop (𝓝 0)
have rw : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop (𝓝 0)
Tactic: rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop (𝓝 0)
have hn : HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ) < 0
Tactic: apply tendsto_zpow_atTop_zero
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (β := ℝ) (fun (x : α) ↦ ‖u x‖) l atTop
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖v x‖) l atTop
have rcases : ∀ (c : ℝ) (hc : c > 0) (hcuv : IsBigOWith c l u v), Tendsto (β := ℝ) (fun (x : α) ↦ ‖v x‖) l atTop
Tactic: rcases huv.exists_pos with ⟨c, hc, hcuv⟩
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (β := ℝ) (fun (x : α) ↦ ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : IsBigOWith c l u v
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖v x‖) l atTop
have hcuv₁ : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
Tactic: rw [IsBigOWith] at hcuv
Cleared hypotheses: hcuv
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (β := ℝ) (fun (x : α) ↦ ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖v x‖) l atTop
have h : ∀ (x : α), ‖v x‖ = c * ‖v x‖ / c
Tactic: convert! Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
α : Type u_2
u v : α → 𝕜
l : Filter α
huv : u =O[l] v
hu : Tendsto (β := ℝ) (fun (x : α) ↦ ‖u x‖) l atTop
c : ℝ
hc : c > 0
hcuv : ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖
x : α
⊢ ‖v x‖ = c * ‖v x‖ / c
have h : ‖v x‖ = ‖v x‖
Tactic: rw [mul_div_cancel_left₀ _ hc.ne.symm]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
⊢ u ^ r ~[l] v ^ r
have obtain : ∀ (φ : α → ℝ) (hφ : Tendsto φ l (𝓝 1)) (huφv : u =ᶠ[l] φ * v), u ^ r ~[l] v ^ r
Tactic: obtain ⟨φ, hφ, huφv⟩ := IsEquivalent.exists_eq_mul h
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ u ^ r ~[l] v ^ r
have rw : ∃ (φ : α → ℝ) (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r
Tactic: rw [isEquivalent_iff_exists_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
have rw : Tendsto ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 (HPow.hPow (α := ℝ) 1 r))
Tactic: rw [← Real.one_rpow r]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ Ne (α := ℝ) 1 0 ∨ 0 ≤ r
have h₁ : Ne (α := ℝ) 1 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
⊢ ∃ (φ : α → ℝ) (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r
have hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
Tactic: have hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1) := by
    rw [← Real.one_rpow r]
    exact Tendsto.comp (Real.continuousAt_rpow_const _ _ (by left; norm_num)) hφ
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
⊢ ∃ (φ : α → ℝ) (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r
have h₁ : u ^ r =ᶠ[l] (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r
Tactic: use (· ^ r) ∘ φ, hφr
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
| u ^ r =ᶠ[l] (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r
have enter : (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r
Tactic: enter [3]
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
| u ^ r =ᶠ[l] (fun (x : ℝ) ↦ x ^ r) ∘ φ * v ^ r
have enter : fun (x : α) ↦ φ x ^ r * v x ^ r
Tactic: enter [3]; change fun x ↦ φ x ^ r * v x ^ r
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)
⊢ u ^ r =ᶠ[l] fun (x : α) ↦ φ x ^ r * v x ^ r
have h₁ : ∀ (x : α) (hφ_pos : 0 < φ x) (huv' : u x = (φ * v) x), (u ^ r) x = φ x ^ r * v x ^ r
Tactic: filter_upwards [Tendsto.eventually_const_lt (zero_lt_one) hφ, huφv] with x hφ_pos huv'
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
⊢ IsEquivalent (E' := ℝ) l (fun (n : α) ↦ Real.log (f n)) fun (n : α) ↦ Real.log (g n)
have hg : ∀ᶠ (x : α) in l, g x ≠ 0
Tactic: have hg := g_tendsto.eventually_ne_atTop 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
⊢ IsEquivalent (E' := ℝ) l (fun (n : α) ↦ Real.log (f n)) fun (n : α) ↦ Real.log (g n)
have hf : ∀ᶠ (x : α) in l, f x ≠ 0
Tactic: have hf := hfg.symm.tendsto_atTop g_tendsto |>.eventually_ne_atTop 0
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : f ~[l] g
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsEquivalent (E' := ℝ) l (fun (n : α) ↦ Real.log (f n)) fun (n : α) ↦ Real.log (g n)
have hfg₁ : Tendsto (f / g) l (𝓝 1)
Tactic: rw [isEquivalent_iff_tendsto_one hg] at hfg
Cleared hypotheses: hfg, g_tendsto, hg, hf
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ l.EventuallyEq (β := ℝ) (fun (x : α) ↦ Real.log ((f / g) x)) fun (n : α) ↦ Real.log (f n) - Real.log (g n)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≠ 0) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≠ 0) x} x →
              Membership.mem (γ := Set α)
                {x : α | (fun (x : α) ↦ (fun (x : α) ↦ Real.log ((f / g) x)) x = Real.log (f x) - Real.log (g x)) x} x}
          x}
    a
Tactic: filter_upwards [hf, hg] with n hf hg using Real.log_div hf hg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≠ 0) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ g x ≠ 0) x} x →
                Membership.mem (γ := Set α)
                  {x : α | (fun (x : α) ↦ (fun (x : α) ↦ Real.log ((f / g) x)) x = Real.log (f x) - Real.log (g x)) x}
                  x}
            x}
      a
⊢ l.EventuallyEq (β := ℝ) (fun (x : α) ↦ Real.log ((f / g) x)) fun (n : α) ↦ Real.log (f n) - Real.log (g n)
have h₁ : ∀ (a : α), f a ≠ 0 → g a ≠ 0 → Real.log ((f / g) a) = Real.log (f a) - Real.log (g a)
Tactic: filter_upwards [hf, hg] with n hf hg using Real.log_div hf hg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ
hfg : Tendsto (f / g) l (𝓝 1)
g_tendsto : Tendsto g l atTop
hg : ∀ᶠ (x : α) in l, g x ≠ 0
hf : ∀ᶠ (x : α) in l, f x ≠ 0
⊢ IsEquivalent (E' := ℝ) l (fun (n : α) ↦ Real.log (f n)) fun (n : α) ↦ Real.log (g n)
have this : Tendsto (fun (n : α) ↦ Real.log (f n) - Real.log (g n)) l (𝓝 (Real.log 1))
Tactic: have := hfg.log (by norm_num) |>.congr' <| by
    filter_upwards [hf, hg] with n hf hg using Real.log_div hf hg
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (hypothesis)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
⊢ IsLittleO.{0, u_1, 0} (E := α) (F := ℝ) atTop (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
have A : ∀ (i : ℕ), ‖g i‖ = g i
Tactic: have A : ∀ i, ‖g i‖ = g i := fun i => Real.norm_of_nonneg (hg i)
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
n : ℕ
⊢ norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
have rwa : Eq (α := ℝ) |∑ i ∈ range n, g i| (∑ i ∈ range n, g i)
Tactic: rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
n : ℕ
rwa : Eq (α := ℝ) |∑ i ∈ range n, g i| (∑ i ∈ range n, g i)
⊢ norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
have rwa₁ : Eq (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range n, g i)
Tactic: rwa [Real.norm_eq_abs, abs_sum_of_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.Asymptotics.SpecificAsymptotics (goal)
Goal:
α : Type u_1
inst : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
n : ℕ
rwa : Eq (α := ℝ) |∑ i ∈ range n, g i| (∑ i ∈ range n, g i)
rwa₁ : Eq (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range n, g i)
⊢ norm (E := ℝ) (∑ i ∈ range n, g i) = ∑ i ∈ range n, g i
have rwa₂ : ∀ (i : ℕ), 0 ≤ g i
Tactic: rwa [Real.norm_eq_abs, abs_sum_of_nonneg']