𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ Tendsto (fun x => eval x P) atTop atTop ↔ 0 < degree P ∧ 0 ≤ leadingCoeff P
refine' ⟨fun h => _, fun h => tendsto_atTop_of_leadingCoeff_nonneg P h.1 h.2⟩
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
have : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop atTop :=
  (isEquivalent_atTop_lead P).tendsto_atTop h
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : 0 < degree P ∧ 0 < leadingCoeff P
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop atTop
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
rw [tendsto_const_mul_pow_atTop_iff, ← pos_iff_ne_zero, natDegree_pos_iff_degree_pos] at this
no goals
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : Tendsto (fun x => eval x P) atTop atTop
this : 0 < degree P ∧ 0 < leadingCoeff P
⊢ 0 < degree P ∧ 0 ≤ leadingCoeff P
exact ⟨this.1, this.2.le⟩