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 𝕜
hdeg : Q.degree < P.degree
hneg : P.leadingCoeff / Q.leadingCoeff < 0
⊢ Q ≠ 0

Tactic:
have hQ : Q ≠ 0 := fun h => by
    simp only [h, div_zero, leadingCoeff_zero] at hneg
    exact hneg.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
hneg : P.leadingCoeff / Q.leadingCoeff < 0
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
hneg : P.leadingCoeff / Q.leadingCoeff < 0
hQ : Q ≠ 0
hdeg₁ : Q.natDegree < P.natDegree
⊢ P.leadingCoeff / Q.leadingCoeff < 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.degree < P.degree
hneg : P.leadingCoeff / Q.leadingCoeff < 0
hQ : Q ≠ 0
hdeg₁ : Q.natDegree < P.natDegree
hneg₁ : P.leadingCoeff / Q.leadingCoeff < 0
⊢ 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
hneg : P.leadingCoeff / Q.leadingCoeff < 0
hQ : Q ≠ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atBot

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

Premises used: Asymptotics.IsEquivalent.tendsto_atBot, 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 : Q.natDegree < P.natDegree
hneg : P.leadingCoeff / Q.leadingCoeff < 0
hQ : Q ≠ 0
refine :
  Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    atBot
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atBot

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

Premises used: Asymptotics.IsEquivalent.tendsto_atBot, 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 : Q.natDegree < P.natDegree
hneg : P.leadingCoeff / Q.leadingCoeff < 0
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
    atBot

Tactic:
apply Tendsto.const_mul_atTop_of_neg hneg

Premises used: Filter.Tendsto.const_mul_atTop_of_neg
-- 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
hneg : P.leadingCoeff / Q.leadingCoeff < 0
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
hneg : P.leadingCoeff / Q.leadingCoeff < 0
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
hnps : P.leadingCoeff / Q.leadingCoeff ≤ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atBot

Tactic:
have ratio_neg : P.leadingCoeff / Q.leadingCoeff < 0 :=
    lt_of_le_of_ne hnps
      (div_ne_zero (fun h => ne_zero_of_degree_gt hdeg <| leadingCoeff_eq_zero.mp h) fun h =>
        hQ <| leadingCoeff_eq_zero.mp h)
  div_tendsto_atBot_of_degree_gt' P Q hdeg ratio_neg

Premises used: Polynomial.ne_zero_of_degree_gt, div_ne_zero, Iff.mp, Polynomial.leadingCoeff_eq_zero, lt_of_le_of_ne, Polynomial.div_tendsto_atBot_of_degree_gt'
-- 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
pos : ∀ (h : 0 ≤ P.leadingCoeff / Q.leadingCoeff), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop
neg : ∀ (h : P.leadingCoeff / Q.leadingCoeff < 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop

Tactic:
by_cases! h : 0 ≤ P.leadingCoeff / Q.leadingCoeff

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 𝕜
hdeg : Q.degree < P.degree
hQ : Q ≠ 0
h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop

Tactic:
tendsto_abs_atTop_atTop.comp (P.div_tendsto_atTop_of_degree_gt Q hdeg hQ h)

Premises used: abs, Polynomial.div_tendsto_atTop_of_degree_gt, Filter.Tendsto.comp, Filter.tendsto_abs_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.degree < P.degree
hQ : Q ≠ 0
h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop

Tactic:
exact tendsto_abs_atTop_atTop.comp (P.div_tendsto_atTop_of_degree_gt Q hdeg hQ h)

Premises used: Polynomial.div_tendsto_atTop_of_degree_gt, Filter.Tendsto.comp, Filter.tendsto_abs_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.degree < P.degree
hQ : Q ≠ 0
h : P.leadingCoeff / Q.leadingCoeff < 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop

Tactic:
tendsto_abs_atBot_atTop.comp (P.div_tendsto_atBot_of_degree_gt Q hdeg hQ h.le)

Premises used: abs, LT.lt.le, Filter.tendsto_abs_atBot_atTop, Polynomial.div_tendsto_atBot_of_degree_gt, Filter.Tendsto.comp
-- 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
h : P.leadingCoeff / Q.leadingCoeff < 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop

Tactic:
exact tendsto_abs_atBot_atTop.comp (P.div_tendsto_atBot_of_degree_gt Q hdeg hQ h.le)

Premises used: LT.lt.le, Filter.tendsto_abs_atBot_atTop, Polynomial.div_tendsto_atBot_of_degree_gt, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
pos :
  ∀ (hP : P = 0),
    IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
neg :
  ∀ (hP : ¬P = 0),
    IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

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 𝕜
hP : P = 0
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
simp [hP, IsEquivalent.refl]

Premises used: Asymptotics.IsEquivalent.refl
-- 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
pos :
  ∀ (hQ : Q = 0),
    IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
neg :
  ∀ (hQ : ¬Q = 0),
    IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
by_cases hQ : Q = 0
-- 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
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

Tactic:
simp [hQ, IsEquivalent.refl]

Premises used: Asymptotics.IsEquivalent.refl
-- 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
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)

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

Premises used: Polynomial.isEquivalent_atBot_lead, Filter.Eventually.mono, Asymptotics.IsEquivalent.div, Filter.eventually_lt_atBot, Asymptotics.IsEquivalent.trans, Filter.EventuallyEq.isEquivalent, OfNat.ofNat, 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 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
neg :
  ∀ (x : 𝕜) (hx : x < 0),
    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' := 𝕜) atBot (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_atBot_lead.symm.div Q.isEquivalent_atBot_lead.symm).symm.trans
      (EventuallyEq.isEquivalent ((eventually_lt_atBot 0).mono fun x hx => ?_))

Premises used: Polynomial.isEquivalent_atBot_lead, Filter.Eventually.mono, Asymptotics.IsEquivalent.div, Filter.eventually_lt_atBot, Asymptotics.IsEquivalent.trans, Filter.EventuallyEq.isEquivalent, OfNat.ofNat, 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 𝕜
hP : ¬P = 0
hQ : ¬Q = 0
x : 𝕜
hx : x < 0
⊢ 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]

Premises used: div_mul_div_comm, zpow_sub₀, 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
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree

Tactic:
rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at hdeg

Premises used: Polynomial.degree_comp_neg_X
-- 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.comp (-X)).degree < (Q.comp (-X)).degree
⊢ Tendsto.{u_1, u_1} (α := 𝕜) (β := 𝕜) ((fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) ∘ Neg.neg) atBot
    (𝓝 0)

Tactic:
(div_tendsto_atTop_zero_of_degree_lt _ _ hdeg).comp tendsto_neg_atBot_atTop

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.div_tendsto_atTop_zero_of_degree_lt, Filter.Tendsto.comp
-- 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.comp (-X)).degree < (Q.comp (-X)).degree
h : ∀ (x : 𝕜), eval x P / eval x Q = ((fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) ∘ Neg.neg) x
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0)

Tactic:
convert! (div_tendsto_atTop_zero_of_degree_lt _ _ hdeg).comp tendsto_neg_atBot_atTop using 2

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.div_tendsto_atTop_zero_of_degree_lt, Filter.Tendsto.comp
-- 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.comp (-X)).degree < (Q.comp (-X)).degree
x : 𝕜
⊢ eval x P / eval x Q = ((fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) ∘ Neg.neg) x

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 𝕜
hQ : Q ≠ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0) ↔ P.degree < Q.degree

Tactic:
⟨fun h ↦ ?_, div_tendsto_atBot_zero_of_degree_lt P Q⟩

Premises used: Polynomial.div_tendsto_atBot_zero_of_degree_lt, Iff.intro
-- 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) atBot (𝓝 0)), P.degree < Q.degree
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0) ↔ P.degree < Q.degree

Tactic:
refine ⟨fun h ↦ ?_, div_tendsto_atBot_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) atBot (𝓝 0)
rw : (P.comp (-X)).degree < (Q.comp (-X)).degree
⊢ P.degree < Q.degree

Tactic:
rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X]

Premises used: Polynomial.degree_comp_neg_X
-- 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) atBot (𝓝 0)
rw : ¬(Q = 0 ∨ eval (coeff (-X) 0) Q = 0 ∧ Eq.{u_1 + 1} (α := 𝕜[X]) (-X) ((C : (a : 𝕜) → 𝕜[X]) (coeff (-X) 0)))
⊢ Q.comp (-X) ≠ 0

Tactic:
rw [Ne, comp_eq_zero_iff]

Premises used: Ne, Polynomial.comp_eq_zero_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) atBot (𝓝 0)
⊢ ¬(Q = 0 ∨ eval (coeff (-X) 0) Q = 0 ∧ Eq.{u_1 + 1} (α := 𝕜[X]) (-X) ((C : (a : 𝕜) → 𝕜[X]) (coeff (-X) 0)))

Tactic:
simp [hQ]
-- 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) atBot (𝓝 0)
⊢ Q.comp (-X) ≠ 0

Tactic:
replace hQ : Q.comp (-X) ≠ 0 := by
    rw [Ne, comp_eq_zero_iff]
    simp [hQ]
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0)
hQ : Q.comp (-X) ≠ 0
rw : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) atTop (𝓝 0)
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree

Tactic:
rw [← div_tendsto_atTop_zero_iff_degree_lt _ _ hQ]

Premises used: Polynomial.div_tendsto_atTop_zero_iff_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 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0)
hQ : Q.comp (-X) ≠ 0
⊢ Tendsto.{u_1, u_1} (α := 𝕜) (β := 𝕜) ((fun (x : 𝕜) ↦ eval x P / eval x Q) ∘ Neg.neg) atTop (𝓝 0)

Tactic:
h.comp tendsto_neg_atTop_atBot

Premises used: Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0)
hQ : Q.comp (-X) ≠ 0
h₁ : ∀ (x : 𝕜), eval x (P.comp (-X)) / eval x (Q.comp (-X)) = ((fun (x : 𝕜) ↦ eval x P / eval x Q) ∘ Neg.neg) x
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) atTop (𝓝 0)

Tactic:
convert! h.comp tendsto_neg_atTop_atBot using 2

Premises used: Filter.tendsto_neg_atTop_atBot, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0)
hQ : Q.comp (-X) ≠ 0
x : 𝕜
⊢ eval x (P.comp (-X)) / eval x (Q.comp (-X)) = ((fun (x : 𝕜) ↦ eval x P / eval x Q) ∘ Neg.neg) x

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 : P.degree = Q.degree
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 (P.leadingCoeff / Q.leadingCoeff))

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

Premises used: Polynomial.isEquivalent_atBot_div, Asymptotics.IsEquivalent.tendsto_nhds, 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 : ℤ))
    atBot (𝓝 (P.leadingCoeff / Q.leadingCoeff))
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 (P.leadingCoeff / Q.leadingCoeff))

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

Premises used: Polynomial.isEquivalent_atBot_div, Asymptotics.IsEquivalent.tendsto_nhds, 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
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atBot (𝓝 (P.leadingCoeff / Q.leadingCoeff))

Tactic:
simp [natDegree_eq_natDegree hdeg]

Premises used: Polynomial.natDegree_eq_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 : Q.degree < P.degree
hQ : Q ≠ 0
⊢ (Q.comp (-X)).degree < (P.comp (-X)).degree

Tactic:
rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at hdeg

Premises used: Polynomial.degree_comp_neg_X
-- 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
hdeg₁ : (Q.comp (-X)).degree < (P.comp (-X)).degree
⊢ Q ≠ 0

Tactic:
rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at hdeg

Premises used: Polynomial.degree_comp_neg_X
-- 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.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q ≠ 0
rw : ¬(Q = 0 ∨ eval (coeff (-X) 0) Q = 0 ∧ Eq.{u_1 + 1} (α := 𝕜[X]) (-X) ((C : (a : 𝕜) → 𝕜[X]) (coeff (-X) 0)))
⊢ Q.comp (-X) ≠ 0

Tactic:
rw [Ne, comp_eq_zero_iff]

Premises used: Ne, Polynomial.comp_eq_zero_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.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q ≠ 0
⊢ ¬(Q = 0 ∨ eval (coeff (-X) 0) Q = 0 ∧ Eq.{u_1 + 1} (α := 𝕜[X]) (-X) ((C : (a : 𝕜) → 𝕜[X]) (coeff (-X) 0)))

Tactic:
simp [hQ]
-- 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.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q ≠ 0
⊢ Q.comp (-X) ≠ 0

Tactic:
replace hQ : Q.comp (-X) ≠ 0 := by
    rw [Ne, comp_eq_zero_iff]
    simp [hQ]
-- 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.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q.comp (-X) ≠ 0
⊢ Tendsto.{u_1, u_1} (α := 𝕜) (β := 𝕜) ((fun (x : 𝕜) ↦ |eval x (P.comp (-X)) / eval x (Q.comp (-X))|) ∘ Neg.neg) atBot
    atTop

Tactic:
(abs_div_tendsto_atTop_atTop_of_degree_gt _ _ hdeg hQ).comp tendsto_neg_atBot_atTop

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.abs_div_tendsto_atTop_atTop_of_degree_gt, Filter.Tendsto.comp
-- 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.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q.comp (-X) ≠ 0
h : ∀ (x : 𝕜), |eval x P / eval x Q| = ((fun (x : 𝕜) ↦ |eval x (P.comp (-X)) / eval x (Q.comp (-X))|) ∘ Neg.neg) x
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atBot atTop

Tactic:
convert! (abs_div_tendsto_atTop_atTop_of_degree_gt _ _ hdeg hQ).comp tendsto_neg_atBot_atTop
    using 2

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.abs_div_tendsto_atTop_atTop_of_degree_gt, Filter.Tendsto.comp
-- 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.comp (-X)).degree < (P.comp (-X)).degree
hQ : Q.comp (-X) ≠ 0
x : 𝕜
⊢ |eval x P / eval x Q| = ((fun (x : 𝕜) ↦ |eval x (P.comp (-X)) / eval x (Q.comp (-X))|) ∘ Neg.neg) x

Tactic:
simp