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