-- Mathlib/Analysis/Polynomial/Basic.lean
theorem tendsto_nhds_iff {c : 𝕜} :
    Tendsto (fun x => eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
exact ⟨_root_.trans hP this, by simp [leadingCoeff_eq_zero.1 hP]⟩

Result:
no goals

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

Tactic:
refine P.isEquivalent_atTop_lead.symm.tendsto_nhds ?_

Result:
case refine_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)

Proof state:
case refine_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun x => c) atTop (𝓝 c)

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.degree ≤ 0

Tactic:
simp [leadingCoeff_eq_zero.1 hP]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
⊢ Tendsto (fun x => eval x P) atTop (𝓝 c) ↔ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩

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

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

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
simp only [hP, zero_mul, tendsto_const_nhds_iff] at this

Result:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
hP : P.leadingCoeff = 0
this : 0 = c
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

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

Tactic:
have := P.isEquivalent_atTop_lead.tendsto_nhds h

Result:
case refine_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
rw [tendsto_const_mul_pow_nhds_iff hP, natDegree_eq_zero_iff_degree_le_zero] at this

Result:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : P.degree ≤ 0 ∧ P.leadingCoeff = c
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Proof state:
case refine_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)

Tactic:
simp only [h.1, this, pow_zero, mul_one]

Result:
case refine_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun x => c) atTop (𝓝 c)

Proof state:
case refine_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
⊢ Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)

Tactic:
have : P.natDegree = 0 := natDegree_eq_zero_iff_degree_le_zero.2 h.2

Result:
case refine_2
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : P.leadingCoeff = c ∧ P.degree ≤ 0
this : P.natDegree = 0
⊢ Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : P.degree ≤ 0 ∧ P.leadingCoeff = c
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
exact this.symm

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

Tactic:
by_cases hP : P.leadingCoeff = 0

Result:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
c : 𝕜
h : Tendsto (fun x => eval x P) atTop (𝓝 c)
this : Tendsto (fun x => P.leadingCoeff * x ^ P.natDegree) atTop (𝓝 c)
hP : ¬P.leadingCoeff = 0
⊢ P.leadingCoeff = c ∧ P.degree ≤ 0