R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
⊢ degree p < degree q
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : p /ₘ q = 0
⊢ degree p < degree q
have := modByMonic_add_div p hq
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
⊢ degree p < degree q
rwa [h, MulZeroClass.mul_zero, add_zero, modByMonic_eq_self_iff hq] at this
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ p /ₘ q = 0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
⊢ p /ₘ q = 0
have : ¬degree q ≤ degree p := not_le_of_gt h
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (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) =
    0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ p /ₘ q = 0
unfold divByMonic divModByMonicAux
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (if h : Monic q then
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).fst
    else 0) =
    0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (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) =
    0
dsimp
no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Nontrivial R
hq : Monic q
h : degree p < degree q
this : ¬degree q ≤ degree p
⊢ (if h : Monic q then
      (if degree q ≤ degree p ∧ ¬p = 0 then
          (↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) +
              (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).fst,
            (divModByMonicAux (p - ↑C (leadingCoeff p) * X ^ (natDegree p - natDegree q) * q) (_ : Monic q)).snd)
        else (0, p)).fst
    else 0) =
    0
rw [dif_pos hq, if_neg (mt And.left this)]