-- Mathlib/Algebra/Polynomial/Div.lean
theorem degree_divByMonic_le (p q : R[X]) : degree (p /ₘ q) ≤ degree p :=
  letI := Classical.decEq R
  if hp0 : p = 0 then by simp only [hp0, zero_divByMonic, le_refl]
  else
    if hq : Monic q then
      if h : degree q ≤ degree p then by
        haveI := Nontrivial.of_polynomial_ne hp0
        rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
          degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
        exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)
      else by
        unfold divByMonic divModByMonicAux
        simp [dif_pos hq, h, if_false, degree_zero, bot_le]
    else (divByMonic_eq_of_not_monic p hq).symm ▸ bot_le

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree ≤ ↑q.natDegree + ↑(p /ₘ q).natDegree

Tactic:
exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
  degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ ↑(p /ₘ q).natDegree ≤ ↑q.natDegree + ↑(p /ₘ q).natDegree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
simp only [hp0, zero_divByMonic, le_refl]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
this✝ : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ p.degree

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
        (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
            let z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
            let_fun _wf := ⋯;
            let dm := (p - q * z).divModByMonicAux ⋯;
            (z + dm.1, dm.2)
          else (0, p)).1
      else 0).degree ≤
    p.degree

Tactic:
simp [dif_pos hq, h, if_false, degree_zero, bot_le]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
unfold divByMonic divModByMonicAux

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
        (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
            let z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
            let_fun _wf := ⋯;
            let dm := (p - q * z).divModByMonicAux ⋯;
            (z + dm.1, dm.2)
          else (0, p)).1
      else 0).degree ≤
    p.degree