case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
by_cases hP : P = 0
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
rw [← natDegree_lt_natDegree_iff hP] at hdeg
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
refine' (isEquivalent_atTop_div P Q).symm.tendsto_nhds _
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 (?neg✝ * 0))

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ 𝕜
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 0)
rw [← MulZeroClass.mul_zero]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ ↑(natDegree P) - ↑(natDegree Q) < 0
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop (𝓝 (?neg✝ * 0))

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ 𝕜
refine' (tendsto_zpow_atTop_zero _).const_mul _
no goals
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree P < natDegree Q
hP : ¬P = 0
⊢ ↑(natDegree P) - ↑(natDegree Q) < 0
linarith
no goals
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree P < degree Q
hP : P = 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop (𝓝 0)
simp [hP, tendsto_const_nhds]