𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
have hQ : Q ≠ 0 := fun h => by
  simp only [h, div_zero, leadingCoeff_zero] at hneg
  exact hneg.false
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
rw [← natDegree_lt_natDegree_iff hQ] at hdeg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atBot
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atBot
refine' (isEquivalent_atTop_div P Q).symm.tendsto_atBot _
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => leadingCoeff P / leadingCoeff Q * x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atBot
apply Tendsto.neg_const_mul_atTop hneg
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ 0 < ↑(natDegree P) - ↑(natDegree Q)
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑(natDegree P) - ↑(natDegree Q))) atTop atTop
apply tendsto_zpow_atTop_atTop
no goals
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : natDegree Q < natDegree P
hneg : leadingCoeff P / leadingCoeff Q < 0
hQ : Q ≠ 0
⊢ 0 < ↑(natDegree P) - ↑(natDegree Q)
linarith
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
h : Q = 0
hneg : 0 < 0
⊢ False
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
hneg : leadingCoeff P / leadingCoeff Q < 0
h : Q = 0
⊢ False
simp only [h, div_zero, leadingCoeff_zero] at hneg
no goals
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : degree Q < degree P
h : Q = 0
hneg : 0 < 0
⊢ False
exact hneg.false