case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0

case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c)
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c) ↔ leadingCoeff P = c ∧ degree P ≤ 0
refine' ⟨fun h => _, fun h => _⟩
case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0
case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0
have := P.isEquivalent_atTop_lead.tendsto_nhds h
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
case refine'_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
⊢ leadingCoeff P = c ∧ degree P ≤ 0
by_cases hP : P.leadingCoeff = 0
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : leadingCoeff P = 0
this : 0 = c
⊢ leadingCoeff P = c ∧ degree P ≤ 0
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
simp only [hP, MulZeroClass.zero_mul, tendsto_const_nhds_iff] at this
no goals
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : leadingCoeff P = 0
this : 0 = c
⊢ leadingCoeff P = c ∧ degree P ≤ 0
refine' ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩
no goals
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : leadingCoeff P = 0
this : 0 = c
⊢ degree P ≤ 0
simp [leadingCoeff_eq_zero.1 hP]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : degree P ≤ 0 ∧ leadingCoeff P = c
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this
no goals
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : degree P ≤ 0 ∧ leadingCoeff P = c
hP : ¬leadingCoeff P = 0
⊢ leadingCoeff P = c ∧ degree P ≤ 0
exact this.symm
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c)
refine' P.isEquivalent_atTop_lead.symm.tendsto_nhds _
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
have : P.natDegree = 0 := natDegree_eq_zero_iff_degree_le_zero.2 h.2
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => c) atTop (𝓝 c)
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => leadingCoeff P * x ^ natDegree P) atTop (𝓝 c)
simp only [h.1, this, pow_zero, mul_one]
no goals
case refine'_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : leadingCoeff P = c ∧ degree P ≤ 0
this : natDegree P = 0
⊢ Tendsto (fun x => c) atTop (𝓝 c)
exact tendsto_const_nhds