R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if h_1 : degree p ≤ degree 0 ∧ 0 ≠ 0 then
          let z := ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p);
          let_fun _wf := (_ : degree (0 - ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p) * p) < degree 0);
          let dm := divModByMonicAux (0 - z * p) (_ : Monic p);
          (z + dm.fst, dm.snd)
        else (0, 0)).snd
    else 0) =
    0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ 0 %ₘ p = 0
unfold modByMonic divModByMonicAux
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if h_1 : degree p ≤ degree 0 ∧ 0 ≠ 0 then
          let z := ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p);
          let_fun _wf := (_ : degree (0 - ↑C (leadingCoeff 0) * X ^ (natDegree 0 - natDegree p) * p) < degree 0);
          let dm := divModByMonicAux (0 - z * p) (_ : Monic p);
          (z + dm.fst, dm.snd)
        else (0, 0)).snd
    else 0) =
    0
dsimp
case pos
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0

case neg
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : ¬Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
by_cases hp : Monic p
no goals
case pos
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
rw [dif_pos hp, if_neg (mt And.right (not_not_intro rfl))]
no goals
case neg
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Ring R
p✝ q p : R[X]
hp : ¬Monic p
⊢ (if h : Monic p then
      (if degree p ≤ ⊥ ∧ ¬0 = 0 then
          (↑C 0 * X ^ (0 - natDegree p) + (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).fst,
            (divModByMonicAux (0 - ↑C 0 * X ^ (0 - natDegree p) * p) (_ : Monic p)).snd)
        else (0, 0)).snd
    else 0) =
    0
rw [dif_neg hp]