-- Mathlib/Analysis/Polynomial/Basic.lean
theorem div_tendsto_zero_iff_degree_lt (hQ : Q ≠ 0) :
    Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) ↔ P.degree < Q.degree

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
⊢ P.degree < Q.degree

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

Result:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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

Proof state:
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ ⊥ < Q.degree

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

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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

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

Result:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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

Proof state:
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : ↑P.natDegree - ↑Q.natDegree = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0
⊢ P.degree < Q.degree

Tactic:
exact absurd h.2 hPQ

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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 ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 0)
⊢ P.degree < Q.degree

Tactic:
rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this

Result:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this : ↑P.natDegree - ↑Q.natDegree = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0 ∨ ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
this : ↑P.natDegree - ↑Q.natDegree = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0 ∨ ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree

Tactic:
rcases this with h | h

Result:
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : ↑P.natDegree - ↑Q.natDegree = 0 ∧ P.leadingCoeff / Q.leadingCoeff = 0
⊢ P.degree < Q.degree

case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) ↔ P.degree < Q.degree

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

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
⊢ P.degree < Q.degree

Proof state:
case pos.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hQ0 : Q.leadingCoeff = 0
⊢ P.degree < Q.degree

Tactic:
exact absurd (leadingCoeff_eq_zero.1 hQ0) hQ

Result:
no goals

Proof state:
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ P.degree < Q.degree

Tactic:
rw [leadingCoeff_eq_zero.1 hP0, degree_zero]

Result:
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ ⊥ < Q.degree

Proof state:
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : P.natDegree < Q.natDegree ∧ 0 = 0
⊢ P.degree < Q.degree

Tactic:
exact degree_lt_degree h.1

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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

Tactic:
rcases hPQ with hP0 | hQ0

Result:
case pos.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hP0 : P.leadingCoeff = 0
⊢ P.degree < Q.degree

case pos.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hQ0 : Q.leadingCoeff = 0
⊢ P.degree < Q.degree

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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

Tactic:
have := (isEquivalent_atTop_div P Q).tendsto_nhds h

Result:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : 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 ^ (↑P.natDegree - ↑Q.natDegree)) atTop (𝓝 0)
⊢ P.degree < Q.degree

Proof state:
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : ↑P.natDegree - ↑Q.natDegree < 0 ∧ 0 = 0
⊢ P.degree < Q.degree

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

Result:
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
h✝ : Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
hPQ : ¬P.leadingCoeff / Q.leadingCoeff = 0
h : P.natDegree < Q.natDegree ∧ 0 = 0
⊢ P.degree < Q.degree