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

case inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
hP : leadingCoeff P ≤ 0
⊢ Tendsto (fun x => abs (eval x P)) atTop atTop
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
⊢ Tendsto (fun x => abs (eval x P)) atTop atTop
cases' le_total 0 P.leadingCoeff with hP hP
no goals
case inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
hP : 0 ≤ leadingCoeff P
⊢ Tendsto (fun x => abs (eval x P)) atTop atTop
exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)
no goals
case inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < degree P
hP : leadingCoeff P ≤ 0
⊢ Tendsto (fun x => abs (eval x P)) atTop atTop
exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)