awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
refine : ∀ (x : ℕ) (hx : 0 < x), HDiv.hDiv (α := EReal) (↑(m * x) : EReal) (↑x : EReal) = (↑m : EReal)
⊢ Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))

Tactic:
refine tendsto_nhds_of_eventually_eq ((eventually_gt_atTop 0).mono fun x hx ↦ ?_)

Premises used: Filter.Eventually.mono, tendsto_nhds_of_eventually_eq, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
x : ℕ
hx : 0 < x
rw : (↑x : EReal) * HDiv.hDiv (α := EReal) (↑m : EReal) (↑x : EReal) = (↑m : EReal)
⊢ HDiv.hDiv (α := EReal) (↑(m * x) : EReal) (↑x : EReal) = (↑m : EReal)

Tactic:
rw [mul_comm, natCast_mul x m, ← mul_div]

Premises used: EReal.natCast_mul, EReal.mul_div, mul_comm
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
x : ℕ
hx : 0 < x
⊢ (↑x : EReal) * HDiv.hDiv (α := EReal) (↑m : EReal) (↑x : EReal) = (↑m : EReal)

Tactic:
mul_div_cancel (natCast_ne_bot x) (natCast_ne_top x) (Nat.cast_ne_zero.2 hx.ne.symm)

Premises used: Iff.mpr, Ne.symm, EReal.mul_div_cancel, EReal.natCast_ne_top, EReal.natCast_ne_bot, Nat.cast_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
x : ℕ
hx : 0 < x
⊢ (↑x : EReal) * HDiv.hDiv (α := EReal) (↑m : EReal) (↑x : EReal) = (↑m : EReal)

Tactic:
exact mul_div_cancel (natCast_ne_bot x) (natCast_ne_top x) (Nat.cast_ne_zero.2 hx.ne.symm)

Premises used: Iff.mpr, Ne.symm, EReal.mul_div_cancel, EReal.natCast_ne_top, EReal.natCast_ne_bot, Nat.cast_ne_zero, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
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))

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)
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
this :
  Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))
⊢ (linearGrowthInf fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * linearGrowthInf u

Tactic:
h.linearGrowthInf_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)

Premises used: Iff.mpr, EReal.natCast_ne_top, Monotone.linearGrowthInf_comp, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
this :
  Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))
⊢ (linearGrowthInf fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * linearGrowthInf u

Tactic:
exact h.linearGrowthInf_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)

Premises used: Iff.mpr, EReal.natCast_ne_top, Monotone.linearGrowthInf_comp, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
this :
  Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))
⊢ (linearGrowthSup fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * linearGrowthSup u

Tactic:
h.linearGrowthSup_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)

Premises used: Iff.mpr, EReal.natCast_ne_top, Monotone.linearGrowthSup_comp, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.LinearGrowth
Goal:
u : ℕ → EReal
m : ℕ
h : Monotone u
hm : m ≠ 0
this :
  Tendsto (β := EReal) (fun (n : ℕ) ↦ HDiv.hDiv (α := EReal) (↑(m * n) : EReal) (↑n : EReal)) atTop (𝓝 (↑m : EReal))
⊢ (linearGrowthSup fun (n : ℕ) ↦ u (m * n)) = (↑m : EReal) * linearGrowthSup u

Tactic:
exact h.linearGrowthSup_comp this (Nat.cast_ne_zero.2 hm) (natCast_ne_top m)

Premises used: Iff.mpr, EReal.natCast_ne_top, Monotone.linearGrowthSup_comp, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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)⁻¹

Tactic:
(h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr ?_)

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left, Real, Filter.IsBoundedUnder.isBigO_const, one_ne_zero', Asymptotics.IsBigO.trans_isLittleO, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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)
refine : Tendsto (Function.comp (β := 𝕜) norm fun (x : 𝕜) ↦ (x - a)⁻¹) (𝓝[≠] a) atTop
⊢ IsLittleO (F := 𝕜) (𝓝[≠] a) f fun (x : 𝕜) ↦ (x - a)⁻¹

Tactic:
refine (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr ?_)

Premises used: Iff.mpr, Asymptotics.isLittleO_const_left, Real, Filter.IsBoundedUnder.isBigO_const, one_ne_zero', Asymptotics.IsBigO.trans_isLittleO, Or.inr
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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)
simp : Tendsto (β := ℝ) (fun (x : 𝕜) ↦ ‖x - a‖⁻¹) (𝓝[≠] a) atTop
⊢ Tendsto (Function.comp (β := 𝕜) norm fun (x : 𝕜) ↦ (x - a)⁻¹) (𝓝[≠] a) atTop

Tactic:
simp only [Function.comp_def, norm_inv]

Premises used: norm_inv, Function.comp_def
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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 (β := ℝ) (fun (x : 𝕜) ↦ ‖x - a‖⁻¹) (𝓝[≠] a) atTop

Tactic:
(tendsto_norm_sub_self_nhdsNE a).inv_tendsto_nhdsGT_zero

Premises used: tendsto_norm_sub_self_nhdsNE, Filter.Tendsto.inv_tendsto_nhdsGT_zero
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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 (β := ℝ) (fun (x : 𝕜) ↦ ‖x - a‖⁻¹) (𝓝[≠] a) atTop

Tactic:
exact (tendsto_norm_sub_self_nhdsNE a).inv_tendsto_nhdsGT_zero

Premises used: tendsto_norm_sub_self_nhdsNE, Filter.Tendsto.inv_tendsto_nhdsGT_zero
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
⊢ NormOneClass R

Tactic:
have noc : NormOneClass R := NormMulClass.toNormOneClass
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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

Tactic:
IsLittleO.of_bound fun c cpos ↦ ?_

Premises used: Asymptotics.IsLittleO.of_bound
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p < q
h : Nontrivial R
noc : NormOneClass R
refine : ∀ (c : ℝ) (cpos : 0 < c), ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ q‖
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q

Tactic:
refine IsLittleO.of_bound fun c cpos ↦ ?_

Premises used: Asymptotics.IsLittleO.of_bound
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
rw : ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ (q - p + p)‖
⊢ ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ q‖

Tactic:
rw [← Nat.sub_add_cancel hpq.le]

Premises used: LT.lt.le, Nat.sub_add_cancel
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
simp_rw : ∃ v ∈ cobounded R, ∀ y ∈ v, ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)
⊢ ∀ᶠ (x : R) in cobounded R, ‖x ^ p‖ ≤ c * ‖x ^ (q - p + p)‖

Tactic:
simp_rw [pow_add, norm_mul, norm_pow, eventually_iff_exists_mem]

Premises used: norm_pow, pow_add, norm_mul, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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)

Tactic:
⟨{y | c⁻¹ ≤ ‖y‖ ^ (q - p)}, ?_, fun y my ↦ ?_⟩

Premises used: Norm.norm, setOf, HSub.hSub, LE.le, Inv.inv, HPow.hPow, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
refine_2 :
  ∀ (y : R) (my : Membership.mem (γ := Set R) {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} y), ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)
⊢ ∃ v ∈ cobounded R, ∀ y ∈ v, ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)

Tactic:
refine ⟨{y | c⁻¹ ≤ ‖y‖ ^ (q - p)}, ?_, fun y my ↦ ?_⟩
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
⊢ 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
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
⊢ ∀ (b : ℝ), ∀ᶠ (a : R) in cobounded R, b ≤ ‖a‖ ^ (q - p)

Tactic:
rw [tendsto_atTop] at key

Premises used: Filter.tendsto_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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 : ∀ (b : ℝ), ∀ᶠ (a : R) in cobounded R, b ≤ ‖a‖ ^ (q - p)
⊢ {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} ∈ cobounded R

Tactic:
mem_map.mp (key c⁻¹)

Premises used: Set.Mem, setOf, Inv.inv, Set.preimage, Iff.mp, Filter.mem_map
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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 : ∀ (b : ℝ), ∀ᶠ (a : R) in cobounded R, b ≤ ‖a‖ ^ (q - p)
⊢ {y : R | c⁻¹ ≤ ‖y‖ ^ (q - p)} ∈ cobounded R

Tactic:
exact mem_map.mp (key c⁻¹)

Premises used: Inv.inv, Iff.mp, Filter.mem_map
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
refine_2 : c⁻¹ * ‖y‖ ^ p ≤ ‖y‖ ^ (q - p) * ‖y‖ ^ p
⊢ ‖y‖ ^ p ≤ c * (‖y‖ ^ (q - p) * ‖y‖ ^ p)

Tactic:
rw [← inv_mul_le_iff₀ cpos]

Premises used: inv_mul_le_iff₀
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
refine_2 : c⁻¹ ≤ ‖y‖ ^ (q - p)
⊢ c⁻¹ * ‖y‖ ^ p ≤ ‖y‖ ^ (q - p) * ‖y‖ ^ p

Tactic:
gcongr
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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‖ ^ (q - p)

Tactic:
my

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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‖ ^ (q - p)

Tactic:
exact my
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
inr : ∀ (h : p < q), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ 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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p : ℕ
hpq : p ≤ p
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ p

Tactic:
isBigO_refl ..

Premises used: Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p : ℕ
hpq : p ≤ p
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ p

Tactic:
exact isBigO_refl ..

Premises used: Asymptotics.isBigO_refl
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p ≤ q
h : p < q
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q

Tactic:
(isLittleO_pow_pow_cobounded_of_lt h).isBigO

Premises used: Asymptotics.IsLittleO.isBigO, Asymptotics.isLittleO_pow_pow_cobounded_of_lt
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : NormMulClass R
p q : ℕ
hpq : p ≤ q
h : p < q
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ p) fun (x : R) ↦ x ^ q

Tactic:
exact (isLittleO_pow_pow_cobounded_of_lt h).isBigO

Premises used: Asymptotics.IsLittleO.isBigO, Asymptotics.isLittleO_pow_pow_cobounded_of_lt
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
apply :
  ∀ (x : 𝕜) (hx : 0 < x),
    Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ x ^ p / x ^ q) x) ((fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) x)
⊢ EventuallyEq (β := 𝕜) atTop (fun (x : 𝕜) ↦ x ^ p / x ^ q) fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)

Tactic:
apply (eventually_gt_atTop (0 : 𝕜)).mono fun x hx => _

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
x : 𝕜
hx : 0 < x
⊢ Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ x ^ p / x ^ q) x) ((fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) x)

Tactic:
simp [zpow_sub₀ hx.ne']

Premises used: zpow_sub₀, LT.lt.ne'
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
apply :
  ∀ (x : 𝕜) (hx : x < 0),
    Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ x ^ p / x ^ q) x) ((fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) x)
⊢ EventuallyEq (β := 𝕜) atBot (fun (x : 𝕜) ↦ x ^ p / x ^ q) fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)

Tactic:
apply (eventually_lt_atBot (0 : 𝕜)).mono fun x hx => _

Premises used: Filter.Eventually.mono, Filter.eventually_lt_atBot, OfNat.ofNat
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
x : 𝕜
hx : x < 0
⊢ Eq.{u_1 + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ x ^ p / x ^ q) x) ((fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) x)

Tactic:
simp [zpow_sub₀ hx.ne]

Premises used: zpow_sub₀, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
rw : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop atTop
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ p / x ^ q) atTop atTop

Tactic:
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]

Premises used: pow_div_pow_eventuallyEq_atTop, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
hn : 0 < HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop atTop

Tactic:
apply tendsto_zpow_atTop_atTop

Premises used: Filter.tendsto_zpow_atTop_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
p q : ℕ
hpq : q < p
⊢ 0 < HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)

Tactic:
lia
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
rw : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop (𝓝 0)
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ p / x ^ q) atTop (𝓝 0)

Tactic:
rw [tendsto_congr' pow_div_pow_eventuallyEq_atTop]

Premises used: pow_div_pow_eventuallyEq_atTop, Filter.tendsto_congr'
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
hn : HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ) < 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ)) atTop (𝓝 0)

Tactic:
apply tendsto_zpow_atTop_zero

Premises used: tendsto_zpow_atTop_zero
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ HSub.hSub (α := ℤ) (↑p : ℤ) (↑q : ℤ) < 0

Tactic:
lia
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ x ^ p) fun (x : 𝕜) ↦ x ^ q

Tactic:
(isLittleO_iff_tendsto' ?_).mpr (tendsto_pow_div_pow_atTop_zero hpq)

Premises used: Iff.mpr, tendsto_pow_div_pow_atTop_zero, Asymptotics.isLittleO_iff_tendsto'
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0

Tactic:
(eventually_gt_atTop 0).mono fun x hx hxq => (pow_ne_zero q hx.ne' hxq).elim

Premises used: False.elim, pow_ne_zero, Filter.Eventually.mono, LT.lt.ne', OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : OrderTopology 𝕜
p q : ℕ
hpq : p < q
⊢ ∀ᶠ (x : 𝕜) in atTop, x ^ q = 0 → x ^ p = 0

Tactic:
exact (eventually_gt_atTop 0).mono fun x hx hxq => (pow_ne_zero q hx.ne' hxq).elim

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
rcases : ∀ (c : ℝ) (hc : c > 0) (hcuv : IsBigOWith c l u v), Tendsto (β := ℝ) (fun (x : α) ↦ ‖v x‖) l atTop
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖v x‖) l atTop

Tactic:
rcases huv.exists_pos with ⟨c, hc, hcuv⟩

Premises used: Asymptotics.IsBigO.exists_pos
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
⊢ ∀ᶠ (x : α) in l, ‖u x‖ ≤ c * ‖v x‖

Tactic:
rw [IsBigOWith] at hcuv

Premises used: Asymptotics.IsBigOWith
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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 : α) ↦ c * ‖v x‖ / c) l atTop

Tactic:
Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)

Premises used: Filter.tendsto_atTop_mono', Filter.Tendsto.atTop_div_const
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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‖
h : ∀ (x : α), ‖v x‖ = c * ‖v x‖ / c
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ ‖v x‖) l atTop

Tactic:
convert! Tendsto.atTop_div_const hc (tendsto_atTop_mono' l hcuv hu)

Premises used: Filter.tendsto_atTop_mono', Filter.Tendsto.atTop_div_const
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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 : α
h h₁ : ‖v x‖ = ‖v x‖
⊢ ‖v x‖ = c * ‖v x‖ / c

Tactic:
rw [mul_div_cancel_left₀ _ hc.ne.symm]

Premises used: mul_div_cancel_left₀, Ne.symm, LT.lt.ne
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
Goal:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
obtain : ∀ (φ : α → ℝ) (hφ : Tendsto φ l (𝓝 1)) (huφv : u =ᶠ[l] φ * v), u ^ r ~[l] v ^ r
⊢ u ^ r ~[l] v ^ r

Tactic:
obtain ⟨φ, hφ, huφv⟩ := IsEquivalent.exists_eq_mul h

Premises used: Asymptotics.IsEquivalent.exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
rw : ∃ (φ : α → ℝ) (_ : Tendsto φ l (𝓝 1)), u ^ r =ᶠ[l] φ * v ^ r
⊢ u ^ r ~[l] v ^ r

Tactic:
rw [isEquivalent_iff_exists_eq_mul]

Premises used: Asymptotics.isEquivalent_iff_exists_eq_mul
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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
rw : Tendsto ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 (HPow.hPow (α := ℝ) 1 r))
⊢ Tendsto (β := ℝ) ((fun (x : ℝ) ↦ x ^ r) ∘ φ) l (𝓝 1)

Tactic:
rw [← Real.one_rpow r]

Premises used: Real.one_rpow
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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₁ : Ne (α := ℝ) 1 0
⊢ Ne (α := ℝ) 1 0 ∨ 0 ≤ r

Tactic:
left
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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

Tactic:
norm_num
-- Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics
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 (𝓝 (HPow.hPow (α := ℝ) 1 r))

Tactic:
exact Tendsto.comp (Real.continuousAt_rpow_const _ _ (by left; norm_num)) hφ

Premises used: Real.continuousAt_rpow_const, Filter.Tendsto.comp