no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : p = 0
⊢ degree (p /ₘ q) ≤ degree p
simp only [hp0, zero_divByMonic, le_refl]
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
this : Nontrivial R
⊢ degree (p /ₘ q) ≤ degree p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
⊢ degree (p /ₘ q) ≤ degree p
haveI := Nontrivial.of_polynomial_ne hp0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
this : Nontrivial R
⊢ ↑(natDegree (p /ₘ q)) ≤ ↑(natDegree q) + ↑(natDegree (p /ₘ q))
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
this : Nontrivial R
⊢ degree (p /ₘ q) ≤ degree p
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))]
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : degree q ≤ degree p
this : Nontrivial R
⊢ ↑(natDegree (p /ₘ q)) ≤ ↑(natDegree q) + ↑(natDegree (p /ₘ q))
exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : ¬degree q ≤ degree p
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).fst
      else 0) ≤
    degree p
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : ¬degree q ≤ degree p
⊢ degree (p /ₘ q) ≤ degree p
unfold divByMonic divModByMonicAux
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : CommRing R
p✝ q✝ p q : R[X]
hp0 : ¬p = 0
hq : Monic q
h : ¬degree q ≤ degree p
⊢ degree
      (if h : Monic q then
        (if h_1 : degree q ≤ degree p ∧ p ≠ 0 then
            let z := ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q);
            let_fun _wf := (_ : degree (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) < degree p);
            let dm := divModByMonicAux (p - z * q) (_ : Monic q);
            (z + dm.fst, dm.snd)
          else (0, p)).fst
      else 0) ≤
    degree p
simp [dif_pos hq, h, false_and_iff, if_false, degree_zero, bot_le]