awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
pos : ∀ (hP : P.leadingCoeff = 0), P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
have neg : ∀ (hP : ¬P.leadingCoeff = 0), P.leadingCoeff = c ∧ P.degree ≤ 0
Tactic: by_cases hP : P.leadingCoeff = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
have this₁ : 0 = c
Tactic: simp only [hP, zero_mul, tendsto_const_nhds_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (hypothesis)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
this : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0
have this₁ : P.degree ≤ 0 ∧ P.leadingCoeff = c
Tactic: rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this
Cleared hypotheses: this, hP
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P) atTop (𝓝 c)
have refine_2 : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
Tactic: refine P.isEquivalent_atTop_lead.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 : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
have this : P.natDegree = 0
Tactic: have : P.natDegree = 0 := natDegree_eq_zero_iff_degree_le_zero.2 h.2
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
have refine_2 : Tendsto (fun (x : 𝕜) ↦ c) atTop (𝓝 c)
Tactic: simp only [h.1, this, pow_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
have h : ∀ (x : 𝕜), eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x
Tactic: convert! (P.comp (-X)).isEquivalent_atTop_lead.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 : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : ∀ (x : 𝕜), eval x P = ((fun (x : 𝕜) ↦ eval x (P.comp (-X))) ∘ Neg.neg) x
⊢ IsEquivalent (E' := 𝕜) atBot (fun (x : 𝕜) ↦ eval x P) fun (x : 𝕜) ↦ P.leadingCoeff * x ^ P.natDegree
have h₁ : ∀ (x : 𝕜),
  P.leadingCoeff * x ^ P.natDegree =
    ((fun (x : 𝕜) ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x
Tactic: convert! (P.comp (-X)).isEquivalent_atTop_lead.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 : 𝕜[X]
inst_3 : OrderTopology 𝕜
x : 𝕜
⊢ P.leadingCoeff * x ^ P.natDegree =
    ((fun (x : 𝕜) ↦ (P.comp (-X)).leadingCoeff * x ^ (P.comp (-X)).natDegree) ∘ Neg.neg) x
have h : P.leadingCoeff * x ^ P.natDegree = (-x) ^ (P.comp (-X)).natDegree * HPow.hPow (α := 𝕜) (-1) P.natDegree * P.leadingCoeff
Tactic: rw [Function.comp_apply, comp_neg_X_leadingCoeff_eq, ← mul_rotate]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
hdeg : 0 < P.degree
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ |eval x P|) atBot atTop
have h : ∀ (x : 𝕜), |eval x P| = ((fun (x : 𝕜) ↦ |eval x (P.comp (-X))|) ∘ Neg.neg) x
Tactic: convert! ((P.comp (-X)).abs_tendsto_atTop (by simp [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 : 𝕜[X]
inst_3 : OrderTopology 𝕜
⊢ (IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|) ↔ P.degree ≤ 0
have refine : ∀ (h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|), P.degree ≤ 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨|P.coeff 0|, eventually_map.mpr (Eventually.of_forall
    (forall_imp (fun _ ↦ le_of_eq) fun x ↦ congr_arg abs <| _root_.trans (congr_arg (eval x)
    (eq_C_of_degree_le_zero h)) eval_C))⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Basic (goal)
Goal:
𝕜 : Type u_1
inst : NormedField 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
P : 𝕜[X]
inst_3 : OrderTopology 𝕜
h : IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|
⊢ P.degree ≤ 0
have contrapose! : ∀ (h : 0 < P.degree), ¬IsBoundedUnder (fun (x1 x2 : 𝕜) ↦ x1 ≤ x2) atBot fun (x : 𝕜) ↦ |eval x P|
Tactic: contrapose! 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 𝕜
⊢ IsEquivalent (E' := 𝕜) atTop (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' := 𝕜) atTop (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' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
⊢ IsEquivalent (E' := 𝕜) atTop (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' := 𝕜) atTop (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' := 𝕜) atTop (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' := 𝕜) atTop (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' := 𝕜) atTop (fun (x : 𝕜) ↦ eval x P / eval x Q) fun (x : 𝕜) ↦
      P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)
⊢ IsEquivalent (E' := 𝕜) atTop (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' := 𝕜) atTop (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' := 𝕜) atTop (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 : 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: refine
    (P.isEquivalent_atTop_lead.symm.div Q.isEquivalent_atTop_lead.symm).symm.trans
      (EventuallyEq.isEquivalent ((eventually_gt_atTop 0).mono fun x hx => ?_))
-- 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) atTop (𝓝 0)
have pos : ∀ (hP : P = 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
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 𝕜
hdeg : P.degree < Q.degree
pos : ∀ (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)
have neg : ∀ (hP : ¬P = 0), Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
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 𝕜
hdeg : P.degree < Q.degree
hP : ¬P = 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
have hdeg₁ : P.natDegree < Q.natDegree
Tactic: rw [← natDegree_lt_natDegree_iff hP] at hdeg
Cleared hypotheses: hdeg, hP
-- 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.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
have neg : Tendsto (β := 𝕜)
  (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
  (𝓝 0)
Tactic: refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_
-- 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.natDegree < Q.natDegree
hP : ¬P = 0
⊢ Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    (𝓝 0)
have neg : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
  atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff * 0))
Tactic: rw [← mul_zero]
-- 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.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))
⊢ Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    (𝓝 0)
have neg₁ : 𝕜
Tactic: rw [← mul_zero]
-- 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) atTop (𝓝 0) ↔ P.degree < Q.degree
have refine : ∀ (h : 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⟩
-- 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) atTop (𝓝 0)
⊢ P.degree < Q.degree
have pos : ∀ (hPQ : P.leadingCoeff / Q.leadingCoeff = 0), P.degree < Q.degree
Tactic: by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 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 𝕜
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
⊢ P.degree < Q.degree
have neg : ∀ (hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0), P.degree < Q.degree
Tactic: by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 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 𝕜
hQ : Q ≠ 0
h : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 0)
hPQ : P.leadingCoeff / Q.leadingCoeff = 0
⊢ P.degree < Q.degree
have hPQ₁ : P.leadingCoeff = 0 ∨ Q.leadingCoeff = 0
Tactic: simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ
Cleared hypotheses: hPQ
-- 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) atTop (𝓝 0)
hPQ : P.leadingCoeff = 0 ∨ Q.leadingCoeff = 0
⊢ P.degree < Q.degree
have pos : ∀ (hP0 : P.leadingCoeff = 0), P.degree < Q.degree
Tactic: rcases hPQ with hP0 | hQ0
Cleared hypotheses: hPQ
-- 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) atTop (𝓝 0)
hPQ : P.leadingCoeff = 0 ∨ Q.leadingCoeff = 0
pos : ∀ (hP0 : P.leadingCoeff = 0), P.degree < Q.degree
⊢ P.degree < Q.degree
have pos₁ : ∀ (hQ0 : Q.leadingCoeff = 0), P.degree < Q.degree
Tactic: rcases hPQ with hP0 | hQ0
Cleared hypotheses: hPQ
-- 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) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ P.degree < Q.degree
have pos : ⊥ < Q.degree
Tactic: rw [leadingCoeff_eq_zero.1 hP0, degree_zero]
-- 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) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
⊢ P.degree < Q.degree
have this : 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
-- 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) 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)
⊢ P.degree < Q.degree
have 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
Tactic: rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this
Cleared hypotheses: this
-- 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) 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
⊢ P.degree < Q.degree
have neg : ∀ (h : HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0),
  P.degree < Q.degree
Tactic: rcases this with h | h
Cleared hypotheses: this
-- 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) 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
⊢ P.degree < Q.degree
have neg₁ : ∀ (h : HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ) < 0 ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0), P.degree < Q.degree
Tactic: rcases this with h | h
Cleared hypotheses: this
-- 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_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.degree < Q.degree
have h₁ : P.natDegree < Q.natDegree ∧ Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] 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 𝕜
hdeg : P.degree = Q.degree
⊢ Tendsto (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
have refine : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
  atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
Tactic: refine (isEquivalent_atTop_div P Q).symm.tendsto_nhds ?_
-- 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 : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ))
    atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
have rw : Tendsto (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑Q.natDegree : ℤ) (↑Q.natDegree : ℤ))
  atTop (𝓝 (P.leadingCoeff / Q.leadingCoeff))
Tactic: rw [show (P.natDegree : ℤ) = Q.natDegree by simp [hdeg, natDegree]]
-- 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
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
h : Q = 0
⊢ False
have hpos₁ : LT.lt.{u_1} (α := 𝕜) 0 0
Tactic: simp only [h, div_zero, leadingCoeff_zero] at hpos
Cleared hypotheses: hpos
-- 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
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atTop
have hQ : Q ≠ 0
Tactic: have hQ : Q ≠ 0 := fun h => by
    simp only [h, div_zero, leadingCoeff_zero] at hpos
    exact hpos.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
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atTop
have hdeg₁ : Q.natDegree < P.natDegree
Tactic: rw [← natDegree_lt_natDegree_iff hQ] at hdeg
Cleared hypotheses: hdeg, hpos, 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
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ eval x P / eval x Q) atTop atTop
have refine : Tendsto (β := 𝕜)
  (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
  atTop
Tactic: refine (isEquivalent_atTop_div P Q).symm.tendsto_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.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (β := 𝕜)
    (fun (x : 𝕜) ↦ P.leadingCoeff / Q.leadingCoeff * x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop
    atTop
have apply : Tendsto (β := 𝕜) (fun (x : 𝕜) ↦ x ^ HSub.hSub (α := ℤ) (↑P.natDegree : ℤ) (↑Q.natDegree : ℤ)) atTop atTop
Tactic: apply Tendsto.const_mul_atTop hpos
-- 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
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
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 (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
h : Q = 0
⊢ False
have hneg₁ : LT.lt.{u_1} (α := 𝕜) 0 0
Tactic: simp only [h, div_zero, leadingCoeff_zero] at hneg
Cleared hypotheses: hneg