-- Mathlib/Analysis/Polynomial/Basic.lean
theorem isBigO_of_degree_le (h : P.degree ≤ Q.degree) :
    (fun x => eval x P) =O[atTop] fun x => eval x Q

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Tactic:
rcases le_iff_lt_or_eq.mp h with h | h

Result:
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree < Q.degree
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree = Q.degree
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Proof state:
case neg.inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree < Q.degree
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Tactic:
exact isBigO_of_div_tendsto_nhds hPQ 0 (div_tendsto_zero_of_degree_lt P Q h)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Tactic:
by_cases hp : P = 0

Result:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Tactic:
have hq : Q ≠ 0 := ne_zero_of_degree_ge_degree h hp

Result:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Proof state:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Tactic:
have hPQ : ∀ᶠ x : 𝕜 in atTop, eval x Q = 0 → eval x P = 0 :=
  Filter.mem_of_superset (Polynomial.eventually_no_roots Q hq) fun x h h' => absurd h' h

Result:
case neg
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Proof state:
case neg.inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h✝ : P.degree ≤ Q.degree
hp : ¬P = 0
hq : Q ≠ 0
hPQ : ∀ᶠ (x : 𝕜) in atTop, eval x Q = 0 → eval x P = 0
h : P.degree = Q.degree
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Tactic:
exact isBigO_of_div_tendsto_nhds hPQ _ (div_tendsto_leadingCoeff_div_of_degree_eq P Q h)

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P Q : 𝕜[X]
inst✝ : OrderTopology 𝕜
h : P.degree ≤ Q.degree
hp : P = 0
⊢ (fun x => eval x P) =O[atTop] fun x => eval x Q

Tactic:
simpa [hp] using isBigO_zero (fun x => eval x Q) atTop

Result:
no goals