-- Mathlib/Analysis/Polynomial/Basic.lean
theorem div_tendsto_atTop_of_degree_gt' (hdeg : Q.degree < P.degree)
    (hpos : 0 < P.leadingCoeff / Q.leadingCoeff) :
    Tendsto (fun x => eval x P / eval x Q) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
h : Q = 0
⊢ False

Tactic:
simp only [h, div_zero, leadingCoeff_zero] at hpos

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
h : Q = 0
hpos : 0 < 0
⊢ False

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop

Tactic:
rw [← natDegree_lt_natDegree_iff hQ] at hdeg

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop atTop

Tactic:
apply Tendsto.const_mul_atTop hpos

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑P.natDegree - ↑Q.natDegree)) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop

Tactic:
have hQ : Q ≠ 0 := fun h => by
  simp only [h, div_zero, leadingCoeff_zero] at hpos
  exact hpos.false

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop

Proof state:
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ 0 < ↑P.natDegree - ↑Q.natDegree

Tactic:
omega

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.degree < P.degree
h : Q = 0
hpos : 0 < 0
⊢ False

Tactic:
exact hpos.false

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => eval x P / eval x Q) atTop atTop

Tactic:
refine (isEquivalent_atTop_div P Q).symm.tendsto_atTop ?_

Result:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => P.leadingCoeff / Q.leadingCoeff * x ^ (↑P.natDegree - ↑Q.natDegree)) atTop atTop

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ Tendsto (fun x => x ^ (↑P.natDegree - ↑Q.natDegree)) atTop atTop

Tactic:
apply tendsto_zpow_atTop_atTop

Result:
case hn
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : Q.natDegree < P.natDegree
hpos : 0 < P.leadingCoeff / Q.leadingCoeff
hQ : Q ≠ 0
⊢ 0 < ↑P.natDegree - ↑Q.natDegree