awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
neg :
  ∀ (x : 𝕜) (hx : 0 < x),
    HDiv.hDiv (α := 𝕜 → 𝕜) (β := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree)
        (fun (x : 𝕜) ↦ Q.leadingCoeff * x ^ Q.natDegree) x =
      (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) x
⊢ IsEquivalent (E' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
refine
    (P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
      (EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => ?_))

Premises used: Polynomial.isEquivalent_atTop_lead, Filter.Eventually.mono, Asymptotics.IsEquivalent.div, Asymptotics.IsEquivalent.trans, Filter.EventuallyEq.isEquivalent, OfNat.ofNat, Asymptotics.IsEquivalent.symm, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
x : 𝕜
hx : 0 < x
⊢ HDiv.hDiv (α := 𝕜 → 𝕜) (β := 𝕜 → 𝕜) (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree)
      (fun (x : 𝕜) ↦ Q.leadingCoeff * x ^ Q.natDegree) x =
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) x

Tactic:
simp [← div_mul_div_comm, zpow_sub₀ hx.ne.symm]

Premises used: div_mul_div_comm, zpow_sub₀, Ne.symm, LT.lt.ne
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree < Q.degree
pos : ∀ (hP : P = 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
neg : ∀ (hP : ¬P = 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)

Tactic:
by_cases hP : P = 0
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree < Q.degree
hP : P = 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)

Tactic:
simp [hP]
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree < Q.degree
hP : ¬P = 0
⊢ P.natDegree < Q.natDegree

Tactic:
rw [← natDegree_lt_natDegree_iff hP] at hdeg

Premises used: Polynomial.natDegree_lt_natDegree_iff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree < Q.degree
hP : ¬P = 0
hdeg₁ : P.natDegree < Q.natDegree
⊢ ¬P = 0

Tactic:
rw [← natDegree_lt_natDegree_iff hP] at hdeg

Premises used: Polynomial.natDegree_lt_natDegree_iff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)

Tactic:
(isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_

Premises used: Asymptotics.IsEquivalent.tendsto_nhds, Polynomial.isEquivalent_atTop_div, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
neg :
  Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    (𝓝 0)
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)

Tactic:
refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_

Premises used: Asymptotics.IsEquivalent.tendsto_nhds, Polynomial.isEquivalent_atTop_div, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
neg :
  Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff * 0))
neg₁ : 𝕜
⊢ Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    (𝓝 0)

Tactic:
rw [← mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff * 0))

Tactic:
(tendsto_zpow_atTop_zero ?_).const_mul _

Premises used: tendsto_zpow_atTop_zero, Filter.Tendsto.const_mul
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.natDegree < Q.natDegree
hP : ¬P = 0
⊢ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) < 0

Tactic:
lia
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0) ↔ P.degree < Q.degree

Tactic:
⟨fun h => ?_, div_tendsto_atTop_zero_of_degree_lt P Q⟩

Premises used: Iff.intro, Polynomial.div_tendsto_atTop_zero_of_degree_lt
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
refine : ∀ (h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)), P.degree < Q.degree
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0) ↔ P.degree < Q.degree

Tactic:
refine ⟨fun h => ?_, div_tendsto_atTop_zero_of_degree_lt P Q⟩
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
pos : ∀ (hPQ : P.leadingCoeff / Q.leadingCoeff = 0), P.degree < Q.degree
neg : ∀ (hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0), P.degree < Q.degree
⊢ P.degree < Q.degree

Tactic:
by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : P.leadingCoeff / Q.leadingCoeff = 0
⊢ P.leadingCoeff = 0 ∨ Q.leadingCoeff = 0

Tactic:
simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ

Premises used: inv_eq_zero, mul_eq_zero, div_eq_mul_inv
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : P.leadingCoeff = 0 ∨ Q.leadingCoeff = 0
pos : ∀ (hP0 : P.leadingCoeff = 0), P.degree < Q.degree
pos₁ : ∀ (hQ0 : Q.leadingCoeff = 0), P.degree < Q.degree
⊢ P.degree < Q.degree

Tactic:
rcases hPQ with hP0 | hQ0
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
pos : ⊥ < Q.degree
⊢ P.degree < Q.degree

Tactic:
rw [leadingCoeff_eq_zero.1 hP0, degree_zero]

Premises used: Polynomial.degree_zero, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ ⊥ < Q.degree

Tactic:
bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')

Premises used: Iff.mpr, bot_lt_iff_ne_bot, Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ ⊥ < Q.degree

Tactic:
exact bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')

Premises used: Iff.mpr, bot_lt_iff_ne_bot, Iff.mp, Polynomial.degree_eq_bot
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hQ0 : Q.leadingCoeff = 0
⊢ P.degree < Q.degree

Tactic:
absurd (leadingCoeff_eq_zero.1 hQ0) hQ

Premises used: absurd, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hQ0 : Q.leadingCoeff = 0
⊢ P.degree < Q.degree

Tactic:
exact absurd (leadingCoeff_eq_zero.1 hQ0) hQ

Premises used: absurd, Iff.mp, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
⊢ Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    (𝓝 0)

Tactic:
have := (isEquivalent_atTop_div P Q).tendsto_nhds h
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this :
  Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    (𝓝 0)
⊢ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0 ∨
    HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) < 0 ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0

Tactic:
rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this

Premises used: tendsto_const_mul_zpow_atTop_nhds_iff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this :
  HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0 ∨
    HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) < 0 ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0
neg :
  ∀ (h : HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0),
    P.degree < Q.degree
neg₁ :
  ∀ (h : HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) < 0 ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0), P.degree < Q.degree
⊢ P.degree < Q.degree

Tactic:
rcases this with h | h
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h_1 : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0
⊢ P.degree < Q.degree

Tactic:
absurd h.2 hPQ

Premises used: absurd, And.right
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h_1 : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0
⊢ P.degree < Q.degree

Tactic:
exact absurd h.2 hPQ

Premises used: absurd, And.right
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h_1 : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) < 0 ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ P.natDegree < Q.natDegree ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0

Tactic:
rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] at h

Premises used: Int.ofNat_lt, zero_add, sub_lt_iff_lt_add
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h_1 : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : P.natDegree < Q.natDegree ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ P.degree < Q.degree

Tactic:
degree_lt_degree h.1

Premises used: And.left, Polynomial.degree_lt_degree
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hQ : Q ≠ 0
h_1 : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : P.natDegree < Q.natDegree ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ P.degree < Q.degree

Tactic:
exact degree_lt_degree h.1

Premises used: And.left, Polynomial.degree_lt_degree
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
(isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_

Premises used: Asymptotics.IsEquivalent.tendsto_nhds, Polynomial.isEquivalent_atTop_div, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree = Q.degree
refine :
  Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_

Premises used: Asymptotics.IsEquivalent.tendsto_nhds, Polynomial.isEquivalent_atTop_div, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Eq (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
simp [hdeg, natDegree]

Premises used: Polynomial.natDegree
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree = Q.degree
rw :
  Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑Q.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
rw [show (P.natDegree : ℤ) = Q.natDegree by simp [hdeg, natDegree]]
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑Q.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
h : Q = 0
⊢ LT.lt.{u_1} (α := 𝕜) 0 0

Tactic:
simp only [h, div_zero, leadingCoeff_zero] at hpos

Premises used: Polynomial.leadingCoeff_zero, div_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
h : Q = 0
hpos : LT.lt.{u_1} (α := 𝕜) 0 0
⊢ False

Tactic:
hpos.false

Premises used: LT.lt.false
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
h : Q = 0
hpos : LT.lt.{u_1} (α := 𝕜) 0 0
⊢ False

Tactic:
exact hpos.false

Premises used: LT.lt.false
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
⊢ Q ≠ 0

Tactic:
have hQ : Q ≠ 0 := fun h => by
    simp only [h, div_zero, leadingCoeff_zero] at hpos
    exact hpos.false
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Q.natDegree < P.natDegree

Tactic:
rw [← natDegree_lt_natDegree_iff hQ] at hdeg

Premises used: Polynomial.natDegree_lt_natDegree_iff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
hdeg₁ : Q.natDegree < P.natDegree
⊢ 0 < P.leadingCoeff / Q.leadingCoeff

Tactic:
rw [← natDegree_lt_natDegree_iff hQ] at hdeg

Premises used: Polynomial.natDegree_lt_natDegree_iff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
hdeg₁ : Q.natDegree < P.natDegree
hpos₁ : 0 < P.leadingCoeff / Q.leadingCoeff
⊢ Q ≠ 0

Tactic:
rw [← natDegree_lt_natDegree_iff hQ] at hdeg

Premises used: Polynomial.natDegree_lt_natDegree_iff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atTop

Tactic:
(isEquivalent_atTop_div P Q).symm.tendsto_atTop ?_

Premises used: Polynomial.isEquivalent_atTop_div, Asymptotics.IsEquivalent.tendsto_atTop, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
refine :
  Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    atTop
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atTop

Tactic:
refine (isEquivalent_atTop_div P Q).symm.tendsto_atTop ?_

Premises used: Polynomial.isEquivalent_atTop_div, Asymptotics.IsEquivalent.tendsto_atTop, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
apply : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop atTop
⊢ Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    atTop

Tactic:
apply Tendsto.const_mul_atTop hpos

Premises used: Filter.Tendsto.const_mul_atTop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
hn : 0 < HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop atTop

Tactic:
apply tendsto_zpow_atTop_atTop

Premises used: Filter.tendsto_zpow_atTop_atTop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ 0 < HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
lia
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
hnng : 0 ≤ P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atTop

Tactic:
have ratio_pos : 0 < P.leadingCoeff / Q.leadingCoeff :=
    lt_of_le_of_ne hnng
      (div_ne_zero (fun h => ne_zero_of_degree_gt hdeg <| leadingCoeff_eq_zero.mp h) fun h =>
          hQ <| leadingCoeff_eq_zero.mp h).symm
  div_tendsto_atTop_of_degree_gt' P Q hdeg ratio_pos

Premises used: Polynomial.div_tendsto_atTop_of_degree_gt', Polynomial.ne_zero_of_degree_gt, Ne.symm, div_ne_zero, Iff.mp, Polynomial.leadingCoeff_eq_zero, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hneg : P.leadingCoeff / Q.leadingCoeff < 0
h : Q = 0
⊢ LT.lt.{u_1} (α := 𝕜) 0 0

Tactic:
simp only [h, div_zero, leadingCoeff_zero] at hneg

Premises used: Polynomial.leadingCoeff_zero, div_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
h : Q = 0
hneg : LT.lt.{u_1} (α := 𝕜) 0 0
⊢ False

Tactic:
hneg.false

Premises used: LT.lt.false
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : Q.degree < P.degree
h : Q = 0
hneg : LT.lt.{u_1} (α := 𝕜) 0 0
⊢ False

Tactic:
exact hneg.false

Premises used: LT.lt.false