case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
by_cases h : P = 0
no goals
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
simp [h, IsEquivalent.refl]
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x =>
      (Finset.sum (range (natDegree P)) fun i => coeff P i * x ^ i) + coeff P (natDegree P) * x ^ natDegree P) ~[atTop]
    fun x => leadingCoeff P * x ^ natDegree P
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x => eval x P) ~[atTop] fun x => leadingCoeff P * x ^ natDegree P
simp only [Polynomial.eval_eq_sum_range, sum_range_succ]
no goals
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : ¬P = 0
⊢ (fun x =>
      (Finset.sum (range (natDegree P)) fun i => coeff P i * x ^ i) + coeff P (natDegree P) * x ^ natDegree P) ~[atTop]
    fun x => leadingCoeff P * x ^ natDegree P
exact
  IsLittleO.add_isEquivalent
    (IsLittleO.sum fun i hi =>
      IsLittleO.const_mul_left
        ((IsLittleO.const_mul_right fun hz => h <| leadingCoeff_eq_zero.mp hz) <|
          isLittleO_pow_pow_atTop_of_lt (mem_range.mp hi))
        _)
    IsEquivalent.refl