no goals
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atBot ↔ 0 < degree P ∧ leadingCoeff P ≤ 0
simp only [← tendsto_neg_atTop_iff, ← eval_neg, tendsto_atTop_iff_leadingCoeff_nonneg,
  degree_neg, leadingCoeff_neg, neg_nonneg]