awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atBot
have hQ : Q ≠ 0
Tactic: have hQ : Q ≠ 0 := fun h => by
    simp only [h, div_zero, leadingCoeff_zero] at hneg
    exact hneg.false
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atBot
have hdeg₁ : Q.natDegree < P.natDegree
Tactic: rw [← natDegree_lt_natDegree_iff hQ] at hdeg
Cleared hypotheses: hdeg, hneg, hQ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
have refine : Tendsto (β := 𝕜)
  (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
  atBot
Tactic: refine (isEquivalent_atTop_div P Q).symm.tendsto_atBot ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    atBot
have apply : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop atTop
Tactic: apply Tendsto.const_mul_atTop_of_neg hneg
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop atTop
have hn : 0 < HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
Tactic: apply tendsto_zpow_atTop_atTop
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop
have pos : ∀ (h : 0 ≤ P.leadingCoeff / Q.leadingCoeff), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop
Tactic: by_cases! h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop
have neg : ∀ (h : P.leadingCoeff / Q.leadingCoeff < 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atTop atTop
Tactic: by_cases! h : 0 ≤ P.leadingCoeff / Q.leadingCoeff
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
have 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 : ℤ)
Tactic: by_cases hP : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 : ℤ)
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
have 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 : ℤ)
Tactic: by_cases hP : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 : ℤ)
have 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 : ℤ)
Tactic: by_cases hQ : Q = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 : ℤ)
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
    P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
have 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 : ℤ)
Tactic: by_cases hQ : Q = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 : ℤ)
have 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
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 => ?_))
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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 (𝓝 0)
have hdeg₁ : (P.comp (-X)).degree < (Q.comp (-X)).degree
Tactic: rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at hdeg
Cleared hypotheses: hdeg
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atBot (𝓝 0)
have h : ∀ (x : 𝕜), eval x P / eval x Q = ((fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) ∘ Neg.neg) x
Tactic: convert! (div_tendsto_atTop_zero_of_degree_lt _ _ hdeg).comp tendsto_neg_atBot_atTop using 2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
have refine : ∀ (h : 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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)
⊢ P.degree < Q.degree
have rw : (P.comp (-X)).degree < (Q.comp (-X)).degree
Tactic: rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
have rw : ¬(Q = 0 ∨ eval (coeff (-X) 0) Q = 0 ∧ Eq.{u_1 + 1} (α := 𝕜[X]) (-X) ((C : (a : 𝕜) → 𝕜[X]) (coeff (-X) 0)))
Tactic: rw [Ne, comp_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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)
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree
have hQ₁ : Q.comp (-X) ≠ 0
Tactic: replace hQ : Q.comp (-X) ≠ 0 := by
    rw [Ne, comp_eq_zero_iff]
    simp [hQ]
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ (P.comp (-X)).degree < (Q.comp (-X)).degree
have rw : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) atTop (𝓝 0)
Tactic: rw [← div_tendsto_atTop_zero_iff_degree_lt _ _ hQ]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 (β := 𝕜) (fun (x : 𝕜) ↦ eval x (P.comp (-X)) / eval x (Q.comp (-X))) atTop (𝓝 0)
have h₁ : ∀ (x : 𝕜), eval x (P.comp (-X)) / eval x (Q.comp (-X)) = ((fun (x : 𝕜) ↦ eval x P / eval x Q) ∘ Neg.neg) x
Tactic: convert! h.comp tendsto_neg_atTop_atBot using 2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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))
have refine : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
  atBot (𝓝 (P.leadingCoeff / Q.leadingCoeff))
Tactic: refine (isEquivalent_atBot_div P Q).symm.tendsto_nhds ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atBot atTop
have hdeg₁ : (Q.comp (-X)).degree < (P.comp (-X)).degree
Tactic: rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at hdeg
Cleared hypotheses: hdeg, hQ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
have rw : ¬(Q = 0 ∨ eval (coeff (-X) 0) Q = 0 ∧ Eq.{u_1 + 1} (α := 𝕜[X]) (-X) ((C : (a : 𝕜) → 𝕜[X]) (coeff (-X) 0)))
Tactic: rw [Ne, comp_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atBot atTop
have hQ₁ : Q.comp (-X) ≠ 0
Tactic: replace hQ : Q.comp (-X) ≠ 0 := by
    rw [Ne, comp_eq_zero_iff]
    simp [hQ]
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P / eval x Q|) atBot atTop
have h : ∀ (x : 𝕜), |eval x P / eval x Q| = ((fun (x : 𝕜) ↦ |eval x (P.comp (-X)) / eval x (Q.comp (-X))|) ∘ Neg.neg) x
Tactic: convert! (abs_div_tendsto_atTop_atTop_of_degree_gt _ _ hdeg hQ).comp tendsto_neg_atBot_atTop
    using 2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : P.degree < Q.degree
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have pos : ∀ (hp : P = 0), IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have neg : ∀ (hp : ¬P = 0), IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
have hq : Q ≠ 0
Tactic: have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h.le hp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have hPQ : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : P.degree < Q.degree
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have h₁ : (P.comp (-X)).degree < (Q.comp (-X)).degree
Tactic: rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have h₁ : ∀ (x : 𝕜), eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x
Tactic: convert! (isLittleO_atTop_of_degree_lt _ _ h).comp_tendsto tendsto_neg_atBot_atTop using 2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsLittleO (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have h₂ : ∀ (x : 𝕜), eval x Q = ((fun (x : 𝕜) ↦ eval x (Q.comp (-X))) ∘ Neg.neg) x
Tactic: convert! (isLittleO_atTop_of_degree_lt _ _ h).comp_tendsto tendsto_neg_atBot_atTop using 2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : P.degree ≤ Q.degree
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have pos : ∀ (hp : P = 0), IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have neg : ∀ (hp : ¬P = 0), IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
have hq : Q ≠ 0
Tactic: have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
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
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have hPQ : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have neg : ∀ (h : P.degree < Q.degree), 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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsBigO (E := 𝕜) (F := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have neg₁ : ∀ (h : P.degree = Q.degree), 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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P Q : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : P.degree ≤ Q.degree
⊢ IsBigO (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have h₁ : (P.comp (-X)).degree ≤ (Q.comp (-X)).degree
Tactic: rw [← P.degree_comp_neg_X, ← Q.degree_comp_neg_X] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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 (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have h₁ : ∀ (x : 𝕜), eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x
Tactic: convert! (isBigO_atTop_of_degree_le _ _ h).comp_tendsto tendsto_neg_atBot_atTop using 2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsBigO (E := 𝕜) (F := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ eval x Q
have h₂ : ∀ (x : 𝕜), eval x Q = ((fun (x : 𝕜) ↦ eval x (Q.comp (-X))) ∘ Neg.neg) x
Tactic: convert! (isBigO_atTop_of_degree_le _ _ h).comp_tendsto tendsto_neg_atBot_atTop using 2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P : R[X]
⊢ IsEquivalent (E' := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ P.leadingCoeff * x ^ P.natDegree
have pos : ∀ (h : P = 0),
  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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsEquivalent (E' := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ P.leadingCoeff * x ^ P.natDegree
have neg : ∀ (h : ¬P = 0),
  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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
have 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
Tactic: simp only [eval_eq_sum_range, sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
R : Type u_2
inst : NormedRing R
inst_1 : NormMulClass R
P Q : R[X]
h : P.degree < Q.degree
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
have pos : ∀ (hP : P = 0), 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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
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
⊢ IsLittleO (E := R) (F := R) (cobounded R) (fun (x : R) ↦ eval x P) fun (x : R) ↦ eval x Q
have neg : ∀ (hP : ¬P = 0), 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