𝕜 : 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)
⊢ degree P < degree Q
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0) ↔ degree P < degree Q
refine' ⟨fun h => _, div_tendsto_zero_of_degree_lt P Q⟩
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 : leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q

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 : ¬leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
𝕜 : 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)
⊢ degree P < degree Q
by_cases hPQ : P.leadingCoeff / Q.leadingCoeff = 0
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 : leadingCoeff P = 0 ∨ leadingCoeff Q = 0
⊢ degree P < degree Q
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 : leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
simp only [div_eq_mul_inv, inv_eq_zero, mul_eq_zero] at hPQ
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 : leadingCoeff P = 0
⊢ degree P < degree Q

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 : leadingCoeff Q = 0
⊢ degree P < degree Q
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 : leadingCoeff P = 0 ∨ leadingCoeff Q = 0
⊢ degree P < degree Q
cases' hPQ with hP0 hQ0
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 : leadingCoeff P = 0
⊢ ⊥ < degree Q
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 : leadingCoeff P = 0
⊢ degree P < degree Q
rw [leadingCoeff_eq_zero.1 hP0, degree_zero]
no goals
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 : leadingCoeff P = 0
⊢ ⊥ < degree Q
exact bot_lt_iff_ne_bot.2 fun hQ' => hQ (degree_eq_bot.1 hQ')
no goals
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 : leadingCoeff Q = 0
⊢ degree P < degree Q
exact absurd (leadingCoeff_eq_zero.1 hQ0) hQ
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 : ¬leadingCoeff P / leadingCoeff Q = 0
this : Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
⊢ degree P < degree Q
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 : ¬leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
have := (isEquivalent_atTop_div P Q).tendsto_nhds h
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 : ¬leadingCoeff P / leadingCoeff Q = 0
this :
  ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0 ∨
    ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
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 : ¬leadingCoeff P / leadingCoeff Q = 0
this : Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
⊢ degree P < degree Q
rw [tendsto_const_mul_zpow_atTop_nhds_iff hPQ] at this
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 : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q

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 : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
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 : ¬leadingCoeff P / leadingCoeff Q = 0
this :
  ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0 ∨
    ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
cases' this with h h
no goals
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 : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) = 0 ∧ leadingCoeff P / leadingCoeff Q = 0
⊢ degree P < degree Q
exact absurd h.2 hPQ
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 : ¬leadingCoeff P / leadingCoeff Q = 0
h : natDegree P < natDegree Q ∧ 0 = 0
⊢ degree P < degree Q
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 : ¬leadingCoeff P / leadingCoeff Q = 0
h : ↑(natDegree P) - ↑(natDegree Q) < 0 ∧ 0 = 0
⊢ degree P < degree Q
rw [sub_lt_iff_lt_add, zero_add, Int.ofNat_lt] at h
no goals
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 : ¬leadingCoeff P / leadingCoeff Q = 0
h : natDegree P < natDegree Q ∧ 0 = 0
⊢ degree P < degree Q
exact degree_lt_degree h.1