awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
inst_1 : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
have have₁ have₂ : ∀ (this : ¬q.degree ≤ p.degree), p %ₘ q = p
have₃ have₄ :
  ∀ (this : ¬q.degree ≤ p.degree),
    (if h : q.Monic then
        (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z :=
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux ⋯;
            (z + dm.1, dm.2)
          else (0, p)).2
      else p) =
      p
have₅ have₆ :
  ∀ (this : ¬q.degree ≤ p.degree),
    (if h : q.Monic then
        (if q.degree ≤ p.degree ∧ ¬p = 0 then
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) +
                ((p -
                        q *
                          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                    ⋯).1,
              ((p -
                      q *
                        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                  ⋯).2)
          else (0, p)).2
      else p) =
      p
⊢ p %ₘ q = p

Tactic:
classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold modByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]

Premises used: dif_pos, Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : Nontrivial R
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
(degree_modByMonic_lt _ hq).le

Premises used: LT.lt.le, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : Nontrivial R
⊢ (p %ₘ q).degree ≤ q.degree

Tactic:
exact (degree_modByMonic_lt _ hq).le

Premises used: LT.lt.le, Polynomial.degree_modByMonic_lt
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
pos : ∀ (hq : q.Monic), (p %ₘ q).degree ≤ p.degree
neg : ∀ (hq : ¬q.Monic), (p %ₘ q).degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
by_cases hq : q.Monic

Premises used: Polynomial.Monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : q.Monic
pos : p.degree < q.degree → (p %ₘ q).degree ≤ p.degree
pos₁ : q.degree ≤ p.degree → (p %ₘ q).degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
cases lt_or_ge (degree p) (degree q)

Premises used: Polynomial.degree, lt_or_ge
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : q.Monic
h_1 : p.degree < q.degree
pos pos₁ : p.degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
rw [(modByMonic_eq_self_iff hq).mpr ‹_›]

Premises used: Polynomial.modByMonic_eq_self_iff, Iff.mpr
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : q.Monic
h_1 : q.degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
(degree_modByMonic_le p hq).trans ‹_›

Premises used: Polynomial.degree_modByMonic_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : q.Monic
h_1 : q.degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
exact (degree_modByMonic_le p hq).trans ‹_›

Premises used: Polynomial.degree_modByMonic_le, LE.le.trans
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : ¬q.Monic
neg neg₁ : p.degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
rw [modByMonic_eq_of_not_monic p hq]

Premises used: Polynomial.modByMonic_eq_of_not_monic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p g : R[X]
hg : g.Monic
⊢ (p %ₘ g).natDegree ≤ g.natDegree

Tactic:
natDegree_le_natDegree (degree_modByMonic_le p hg)

Premises used: Polynomial.natDegree_le_natDegree, Polynomial.degree_modByMonic_le
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ (p %ₘ q).natDegree ≤ p.natDegree

Tactic:
natDegree_le_natDegree degree_modByMonic_le_left

Premises used: Polynomial.natDegree_le_natDegree, Polynomial.degree_modByMonic_le_left
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ X ∣ HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) (p.coeff 0) : R[X])

Tactic:
simp [X_dvd_iff, coeff_C]

Premises used: Polynomial.coeff_C, Polynomial.X_dvd_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
⊢ (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree <
    p.degree

Tactic:
have _wf := div_wf_lemma h hq
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree <
    p.degree
⊢ (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) %ₘ
      q =
    p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q)

Tactic:
have ih := modByMonic_eq_sub_mul_div
          (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) q
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree <
    p.degree
ih :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) %ₘ
      q =
    p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q)
unfold :
  (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
unfold modByMonic divByMonic divModByMonicAux

Premises used: Polynomial.divByMonic, Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree <
    p.degree
ih :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) %ₘ
      q =
    p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q)
rw :
  (have z :=
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
rw [dif_pos hq, dif_pos h]

Premises used: dif_pos
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree <
    p.degree
ih :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) %ₘ
      q =
    p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q)
⊢ ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
        hq).2 =
    p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q)

Tactic:
rw [modByMonic, dif_pos hq] at ih

Premises used: dif_pos, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree <
    p.degree
ih :
  ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
        hq).2 =
    p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q)
⊢ (have z :=
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
ih.trans ?_

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : q.degree ≤ p.degree ∧ p ≠ 0
_wf :
  (p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree <
    p.degree
ih :
  ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
        hq).2 =
    p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q)
refine :
  p -
        q *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) -
      q *
        ((p -
            q *
              HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))) /ₘ
          q) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
⊢ (have z :=
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
      have _wf := ⋯;
      have dm := (p - q * z).divModByMonicAux ⋯;
      (z + dm.1, dm.2)).2 =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
refine ih.trans ?_

Premises used: Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
unfold :
  (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
unfold modByMonic divByMonic divModByMonicAux

Premises used: Polynomial.divByMonic, Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
dsimp :
  (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) +
              ((p -
                      q *
                        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                  ⋯).1,
            ((p -
                    q *
                      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                        (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                ⋯).2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if q.degree ≤ p.degree ∧ ¬p = 0 then
              (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                    (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) +
                  ((p -
                          q *
                            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                      ⋯).1,
                ((p -
                        q *
                          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                    ⋯).2)
            else (0, p)).1
        else 0
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
              have z :=
                HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                  (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
              have _wf := ⋯;
              have dm := (p - q * z).divModByMonicAux ⋯;
              (z + dm.1, dm.2)
            else (0, p)).1
        else 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
rw : p = p - q * (p /ₘ q)
rw₁ : p = p - q * 0
rw₂ : p = p - 0
rw₃ rw₄ : p = p
⊢ p %ₘ q = p - q * (p /ₘ q)

Tactic:
rw [modByMonic_eq_of_not_monic _ hq, divByMonic_eq_of_not_monic _ hq, mul_zero, sub_zero]

Premises used: Polynomial.divByMonic_eq_of_not_monic, sub_zero, Polynomial.modByMonic_eq_of_not_monic, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ p %ₘ q + q * (p /ₘ q) = p

Tactic:
eq_sub_iff_add_eq.1 (modByMonic_eq_sub_mul_div p q)

Premises used: eq_sub_iff_add_eq, Polynomial.modByMonic_eq_sub_mul_div, Iff.mp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
inst_1 : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
⊢ p %ₘ q + q * (p /ₘ q) = p

Tactic:
have := modByMonic_add_div p q
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
inst_1 : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
rwa : ∀ (this : p %ₘ q + q * 0 = p), p.degree < q.degree
rwa₁ : ∀ (this : p %ₘ q + 0 = p), p.degree < q.degree
rwa₂ : ∀ (this : p %ₘ q = p), p.degree < q.degree
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (this : p.degree < q.degree), p.degree < q.degree
⊢ p.degree < q.degree

Tactic:
rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this

Premises used: Polynomial.modByMonic_eq_self_iff, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
inst_1 : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
unfold :
  Eq.{u + 1} (α := R[X])
    (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0)
    0
⊢ p /ₘ q = 0

Tactic:
unfold divByMonic divModByMonicAux

Premises used: Polynomial.divByMonic, Polynomial.divModByMonicAux
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
inst_1 : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
dsimp :
  Eq.{u + 1} (α := R[X])
    (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) +
              ((p -
                      q *
                        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                  ⋯).1,
            ((p -
                    q *
                      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                        (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                ⋯).2)
        else (0, p)).1
    else 0)
    0
⊢ Eq.{u + 1} (α := R[X])
    (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree));
          have _wf := ⋯;
          have dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0)
    0

Tactic:
dsimp