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 𝕜
h : P.degree < Q.degree
pos : ∀ (hp : P = 0), IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
neg : ∀ (hp : ¬P = 0), IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

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 𝕜
h : P.degree < Q.degree
hp : P = 0
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

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 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
⊢ Q ≠ 0

Tactic:
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h.le hp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
hq : Q ≠ 0
⊢ ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0

Tactic:
have hPQ : ∀ᶠ x in atTop, Q.eval x = 0 → P.eval x = 0 :=
      mem_of_superset (eventually_atTop_not_isRoot Q hq) fun x h h' ↦ absurd 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 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
isLittleO_of_tendsto' hPQ (div_tendsto_atTop_zero_of_degree_lt P Q h)

Premises used: Asymptotics.isLittleO_of_tendsto', 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 𝕜
h : P.degree < Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
exact isLittleO_of_tendsto' hPQ (div_tendsto_atTop_zero_of_degree_lt P Q h)

Premises used: Asymptotics.isLittleO_of_tendsto', 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 𝕜
h : 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 h

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 𝕜
h : (P.comp (-X)).degree < (Q.comp (-X)).degree
⊢ IsLittleO.{u_1, u_1, u_1} (α := 𝕜) (E := 𝕜) (F := 𝕜) atBot ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg)
    ((fun (x : 𝕜) ↦ eval x (Q.comp (-X))) ∘ Neg.neg)

Tactic:
(isLittleO_atTop_of_degree_lt _ _ h).comp_tendsto tendsto_neg_atBot_atTop

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.isLittleO_atTop_of_degree_lt, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : (P.comp (-X)).degree < (Q.comp (-X)).degree
h₁ : ∀ (x : 𝕜), eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x
h₂ : ∀ (x : 𝕜), eval x Q = ((fun (x : 𝕜) ↦ eval x (Q.comp (-X))) ∘ Neg.neg) x
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
convert! (isLittleO_atTop_of_degree_lt _ _ h).comp_tendsto tendsto_neg_atBot_atTop using 2

Premises used: Filter.tendsto_neg_atBot_atTop, Polynomial.isLittleO_atTop_of_degree_lt, Asymptotics.IsLittleO.comp_tendsto
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : (P.comp (-X)).degree < (Q.comp (-X)).degree
x : 𝕜
⊢ eval x P = ((fun (x : 𝕜) ↦ eval x (P.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 𝕜
h : (P.comp (-X)).degree < (Q.comp (-X)).degree
x : 𝕜
⊢ eval x Q = ((fun (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 𝕜
h : P.degree ≤ Q.degree
pos : ∀ (hp : P = 0), IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
neg : ∀ (hp : ¬P = 0), IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

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 𝕜
h : P.degree ≤ Q.degree
hp : P = 0
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
simpa [hp] using isBigO_zero Q.eval atTop

Premises used: Polynomial.eval, Asymptotics.isBigO_zero, Filter.atTop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
⊢ Q ≠ 0

Tactic:
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
⊢ ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0

Tactic:
have hPQ : ∀ᶠ x in atTop, Q.eval x = 0 → P.eval x = 0 :=
      mem_of_superset (eventually_atTop_not_isRoot Q hq) fun x h h' ↦ absurd 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 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
neg : ∀ (h : P.degree < Q.degree), IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
neg₁ : ∀ (h : P.degree = Q.degree), IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
rcases le_iff_lt_or_eq.mp h with h | h

Premises used: le_iff_lt_or_eq, Iff.mp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h_1 : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree < Q.degree
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_atTop_zero_of_degree_lt P Q h)

Premises used: Asymptotics.isBigO_of_div_tendsto_nhds, Polynomial.div_tendsto_atTop_zero_of_degree_lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h_1 : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree < Q.degree
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
exact isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_atTop_zero_of_degree_lt P Q h)

Premises used: Asymptotics.isBigO_of_div_tendsto_nhds, Polynomial.div_tendsto_atTop_zero_of_degree_lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h_1 : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree = Q.degree
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
isBigO_of_div_tendsto_nhds hPQ _ (div_tendsto_atTop_leadingCoeff_div_of_degree_eq P Q h)

Premises used: Polynomial.div_tendsto_atTop_leadingCoeff_div_of_degree_eq, Asymptotics.isBigO_of_div_tendsto_nhds
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h_1 : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree = Q.degree
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
exact isBigO_of_div_tendsto_nhds hPQ _ (div_tendsto_atTop_leadingCoeff_div_of_degree_eq P Q h)

Premises used: Polynomial.div_tendsto_atTop_leadingCoeff_div_of_degree_eq, Asymptotics.isBigO_of_div_tendsto_nhds
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : 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 h

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 𝕜
h : (P.comp (-X)).degree ≤ (Q.comp (-X)).degree
⊢ IsBigO.{u_1, u_1, u_1} (α := 𝕜) (E := 𝕜) (F := 𝕜) atBot ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg)
    ((fun (x : 𝕜) ↦ eval x (Q.comp (-X))) ∘ Neg.neg)

Tactic:
(isBigO_atTop_of_degree_le _ _ h).comp_tendsto tendsto_neg_atBot_atTop

Premises used: Filter.tendsto_neg_atBot_atTop, Asymptotics.IsBigO.comp_tendsto, Polynomial.isBigO_atTop_of_degree_le
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : (P.comp (-X)).degree ≤ (Q.comp (-X)).degree
h₁ : ∀ (x : 𝕜), eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x
h₂ : ∀ (x : 𝕜), eval x Q = ((fun (x : 𝕜) ↦ eval x (Q.comp (-X))) ∘ Neg.neg) x
⊢ IsBigO (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q

Tactic:
convert! (isBigO_atTop_of_degree_le _ _ h).comp_tendsto tendsto_neg_atBot_atTop using 2

Premises used: Filter.tendsto_neg_atBot_atTop, Asymptotics.IsBigO.comp_tendsto, Polynomial.isBigO_atTop_of_degree_le
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : (P.comp (-X)).degree ≤ (Q.comp (-X)).degree
x : 𝕜
⊢ eval x P = ((fun (x : 𝕜) ↦ eval x (P.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 𝕜
h : (P.comp (-X)).degree ≤ (Q.comp (-X)).degree
x : 𝕜
⊢ eval x Q = ((fun (x : 𝕜) ↦ eval x (Q.comp (-X))) ∘ Neg.neg) x

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : CommRing R
inst_1 : IsDomain R
P : R[X]
hP : P ≠ 0
⊢ ∀ᶠ (x : R) in cofinite, ¬P.IsRoot x

Tactic:
(finite_setOf_isRoot hP).compl_mem_cofinite

Premises used: Set.Mem, Polynomial.IsRoot, Filter.Eventually, setOf, Set.Finite.compl_mem_cofinite, Polynomial.finite_setOf_isRoot
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P : R[X]
pos :
  ∀ (h : P = 0),
    IsEquivalent (E' := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ P.leadingCoeff * x ^ P.natDegree
neg :
  ∀ (h : ¬P = 0),
    IsEquivalent (E' := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ P.leadingCoeff * x ^ P.natDegree
⊢ IsEquivalent (E' := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
by_cases h : P = 0
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P : R[X]
h : P = 0
⊢ IsEquivalent (E' := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
simp [h, IsEquivalent.refl]

Premises used: Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P : R[X]
h : ¬P = 0
neg :
  IsEquivalent (E' := R) (cobounded R)
    (fun (x : R) ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) fun (x : R) ↦
    P.leadingCoeff * x ^ P.natDegree
⊢ IsEquivalent (E' := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ P.leadingCoeff * x ^ P.natDegree

Tactic:
simp only [eval_eq_sum_range, sum_range_succ]

Premises used: Polynomial.eval_eq_sum_range, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P : R[X]
h : ¬P = 0
⊢ IsEquivalent (E' := R) (cobounded R)
    (fun (x : R) ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) fun (x : R) ↦
    P.leadingCoeff * x ^ P.natDegree

Tactic:
(IsLittleO.sum fun i hi ↦
      ((isLittleO_pow_pow_cobounded_of_lt (mem_range.mp hi)).const_mul_right
        (leadingCoeff_ne_zero.mpr h)).const_mul_left _).add_isEquivalent .refl

Premises used: Iff.mpr, Asymptotics.IsLittleO.sum, Asymptotics.IsLittleO.const_mul_left, Finset.mem_range, Polynomial.leadingCoeff_ne_zero, Asymptotics.IsEquivalent.refl, Iff.mp, Asymptotics.IsLittleO.const_mul_right, Asymptotics.IsLittleO.add_isEquivalent, Asymptotics.isLittleO_pow_pow_cobounded_of_lt
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P : R[X]
h : ¬P = 0
⊢ IsEquivalent (E' := R) (cobounded R)
    (fun (x : R) ↦ ∑ i ∈ range P.natDegree, P.coeff i * x ^ i + P.coeff P.natDegree * x ^ P.natDegree) fun (x : R) ↦
    P.leadingCoeff * x ^ P.natDegree

Tactic:
exact (IsLittleO.sum fun i hi ↦
      ((isLittleO_pow_pow_cobounded_of_lt (mem_range.mp hi)).const_mul_right
        (leadingCoeff_ne_zero.mpr h)).const_mul_left _).add_isEquivalent .refl

Premises used: Iff.mpr, Asymptotics.IsLittleO.sum, Asymptotics.IsLittleO.const_mul_left, Finset.mem_range, Polynomial.leadingCoeff_ne_zero, Asymptotics.IsEquivalent.refl, Iff.mp, Asymptotics.IsLittleO.const_mul_right, Asymptotics.IsLittleO.add_isEquivalent, Asymptotics.isLittleO_pow_pow_cobounded_of_lt
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
pos : ∀ (hP : P = 0), IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
neg : ∀ (hP : ¬P = 0), IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
by_cases hP : P = 0
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : P = 0
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
simp [hP]
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm

Premises used: Asymptotics.IsEquivalent.trans_isLittleO, Asymptotics.IsLittleO.trans_isEquivalent, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
neg : Q.leadingCoeff ≠ 0
neg₁ : IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
refine isEquivalent_cobounded_leading_monomial.trans_isLittleO <|
      ((IsLittleO.const_mul_right ?_ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm

Premises used: Asymptotics.IsEquivalent.trans_isLittleO, Asymptotics.IsLittleO.trans_isEquivalent, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ Q.leadingCoeff ≠ 0

Tactic:
leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt h)

Premises used: Iff.mpr, Polynomial.ne_zero_of_degree_gt, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ Q.leadingCoeff ≠ 0

Tactic:
exact leadingCoeff_ne_zero.mpr (ne_zero_of_degree_gt h)

Premises used: Iff.mpr, Polynomial.ne_zero_of_degree_gt, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree

Tactic:
isLittleO_pow_pow_cobounded_of_lt (natDegree_lt_natDegree hP h)

Premises used: Polynomial.natDegree_lt_natDegree, Asymptotics.isLittleO_pow_pow_cobounded_of_lt
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
hP : ¬P = 0
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree

Tactic:
exact isLittleO_pow_pow_cobounded_of_lt (natDegree_lt_natDegree hP h)

Premises used: Polynomial.natDegree_lt_natDegree, Asymptotics.isLittleO_pow_pow_cobounded_of_lt
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
pos :
  ∀ (hQ : Q.leadingCoeff = 0), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
neg :
  ∀ (hQ : ¬Q.leadingCoeff = 0), IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
by_cases hQ : Q.leadingCoeff = 0

Premises used: Polynomial.leadingCoeff
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : Q.leadingCoeff = 0
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
aesop
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : ¬Q.leadingCoeff = 0
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
isEquivalent_cobounded_leading_monomial.trans_isBigO <|
      ((IsBigO.const_mul_right hQ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.IsEquivalent.trans_isBigO, Asymptotics.IsBigO.const_mul_right, Asymptotics.IsBigO.trans_isEquivalent, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : ¬Q.leadingCoeff = 0
neg : IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q

Tactic:
refine isEquivalent_cobounded_leading_monomial.trans_isBigO <|
      ((IsBigO.const_mul_right hQ ?_).const_mul_left _).trans_isEquivalent
        isEquivalent_cobounded_leading_monomial.symm

Premises used: Asymptotics.IsBigO.const_mul_left, Asymptotics.IsEquivalent.trans_isBigO, Asymptotics.IsBigO.const_mul_right, Asymptotics.IsBigO.trans_isEquivalent, Asymptotics.IsEquivalent.symm
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : ¬Q.leadingCoeff = 0
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree

Tactic:
isBigO_pow_pow_cobounded_of_le (natDegree_le_natDegree h)

Premises used: Polynomial.natDegree_le_natDegree, Asymptotics.isBigO_pow_pow_cobounded_of_le
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree ≤ Q.degree
hQ : ¬Q.leadingCoeff = 0
⊢ IsBigO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ x ^ P.natDegree) fun (x : R) ↦ x ^ Q.natDegree

Tactic:
exact isBigO_pow_pow_cobounded_of_le (natDegree_le_natDegree h)

Premises used: Polynomial.natDegree_le_natDegree, Asymptotics.isBigO_pow_pow_cobounded_of_le
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
⊢ IsLittleO (E := ℤ) (F := ℤ) (Bornology.cobounded ℤ) (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P

Tactic:
have o := isLittleO_cobounded_of_degree_lt h
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) (Bornology.cobounded ℤ) (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
⊢ IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P

Tactic:
rw [IsOrderBornology.cobounded_eq, ← Int.cofinite_eq] at o

Premises used: Int.cofinite_eq, IsOrderBornology.cobounded_eq
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
⊢ ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x

Tactic:
have nr := eventually_cofinite_not_isRoot (ne_zero_of_degree_gt h)
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
⊢ ∀ (x : ℤ), ¬P.IsRoot x ↔ 0 < ‖eval x P‖

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
⊢ ∀ᶠ (x : ℤ) in cofinite, ‖eval x Q‖ < ‖eval x P‖

Tactic:
have key := o.eventuallyLT_norm_of_eventually_pos (nr.congr (.of_forall (by simp)))
-- Module: Mathlib.Analysis.Polynomial.Basic
Goal:
P Q : ℤ[X]
h : Q.degree < P.degree
o : IsLittleO (E := ℤ) (F := ℤ) cofinite (fun (x : ℤ) ↦ eval x Q) fun (x : ℤ) ↦ eval x P
nr : ∀ᶠ (x : ℤ) in cofinite, ¬P.IsRoot x
key : ∀ᶠ (x : ℤ) in cofinite, ‖eval x Q‖ < ‖eval x P‖
⊢ Set.Finite (α := ℤ) {x : ℤ | LE.le (α := ℝ) |(↑(eval x P) : ℝ)| |(↑(eval x Q) : ℝ)|}

Tactic:
simp_rw [eventually_cofinite, not_lt, Int.norm_eq_abs] at key

Premises used: Filter.eventually_cofinite, Int.norm_eq_abs, not_lt