awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
⊢ q.degree ≤ p.degree

Tactic:
exact h.1

Premises used: And.left
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree)) *
        q).degree
rw₁ :
  p.degree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree +
      q.degree
rw₂ : p.degree = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
rw₃ : (↑p.natDegree : WithBot ℕ) = (↑(p.natDegree - q.natDegree) : WithBot ℕ) + q.degree
rw₄ :
  (↑p.natDegree : WithBot ℕ) =
    HAdd.hAdd (α := WithBot ℕ) (↑(p.natDegree - q.natDegree) : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
rw₅ : Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(p.natDegree - q.natDegree + q.natDegree) : WithBot ℕ)
rw₆ rw₇ : Eq (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑p.natDegree : WithBot ℕ)
⊢ p.degree =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).degree

Tactic:
rw [hq.degree_mul_comm, hq.degree_mul, degree_C_mul_X_pow _ hp, degree_eq_natDegree h.2,
        degree_eq_natDegree hq0, ← Nat.cast_add, tsub_add_cancel_of_le hlt]

Premises used: Polynomial.degree_eq_natDegree, tsub_add_cancel_of_le, Nat.cast_add, And.right, Polynomial.Monic.degree_mul, Polynomial.degree_C_mul_X_pow, Polynomial.Monic.degree_mul_comm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree ≤ p.degree ∧ p ≠ 0
hq : q.Monic
hp : p.leadingCoeff ≠ 0
hq0 : q ≠ 0
hlt : q.natDegree ≤ p.natDegree
rw :
  p.leadingCoeff =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).leadingCoeff
rw₁ : p.leadingCoeff = leadingCoeff ((C : (a : R) → R[X]) p.leadingCoeff)
rw₂ rw₃ : p.leadingCoeff = p.leadingCoeff
⊢ p.leadingCoeff =
    (q *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).leadingCoeff

Tactic:
rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C]

Premises used: Polynomial.leadingCoeff_mul_X_pow, Polynomial.leadingCoeff_monic_mul, Polynomial.leadingCoeff_C
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
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.1, h.2⟩ hq
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
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).degree <
    q.degree

Tactic:
have :=
        degree_modByMonic_lt (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this_1 : DecidableEq R := Classical.decEq R
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
this :
  ((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).degree <
    q.degree
⊢ (p %ₘ q).degree < q.degree

Tactic:
grind [divModByMonicAux, modByMonic]

Premises used: Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
unfold :
  ∀ (h : ¬q.degree ≤ p.degree),
    degree.{u} (R := R)
        (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) <
      q.degree
⊢ ∀ (h : ¬q.degree ≤ p.degree), (p %ₘ q).degree < q.degree

Tactic:
unfold modByMonic divModByMonicAux

Premises used: Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
dsimp :
  ∀ (h : ¬q.degree ≤ p.degree),
    degree.{u} (R := R)
        (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) <
      q.degree
⊢ ∀ (h : ¬q.degree ≤ p.degree),
    degree.{u} (R := R)
        (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) <
      q.degree

Tactic:
dsimp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
rw : ∀ (h : ¬q.degree ≤ p.degree), (0, p).2.degree < q.degree
⊢ ∀ (h : ¬q.degree ≤ p.degree),
    degree.{u} (R := R)
        (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) <
      q.degree

Tactic:
rw [dif_pos hq, if_neg h]

Premises used: dif_pos, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ∀ (h : ¬q.degree ≤ p.degree), (0, p).2.degree < q.degree

Tactic:
lt_of_not_ge

Premises used: lt_of_not_ge
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ ∀ (h : ¬q.degree ≤ p.degree), (0, p).2.degree < q.degree

Tactic:
exact lt_of_not_ge

Premises used: lt_of_not_ge
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
unfold :
  degree.{u} (R := R)
      (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) <
    q.degree
⊢ (p %ₘ q).degree < q.degree

Tactic:
unfold modByMonic divModByMonicAux

Premises used: Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
dsimp :
  degree.{u} (R := R)
      (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) <
    q.degree
⊢ degree.{u} (R := R)
      (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) <
    q.degree

Tactic:
dsimp
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
rw : degree.{u} (R := R) (0, 0).2 < q.degree
⊢ degree.{u} (R := R)
      (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) <
    q.degree

Tactic:
rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]

Premises used: Classical.not_not, dif_pos, Iff.mp, if_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree.{u} (R := R) (0, 0).2 < q.degree

Tactic:
lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero))

Premises used: mt, Ne.symm, Iff.mp, bot_le, Polynomial.degree_eq_bot, lt_of_le_of_ne, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
hp : ¬p ≠ 0
⊢ degree.{u} (R := R) (0, 0).2 < q.degree

Tactic:
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 hq.ne_zero))

Premises used: mt, Ne.symm, Iff.mp, bot_le, Polynomial.degree_eq_bot, lt_of_le_of_ne, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
pos : ∀ (hpq : p %ₘ q = 0), (p %ₘ q).natDegree < q.natDegree
neg : ∀ (hpq : ¬p %ₘ q = 0), (p %ₘ q).natDegree < q.natDegree
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
by_cases hpq : p %ₘ q = 0
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
pos : q.natDegree ≠ 0
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero, Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
pos : ∀ (hq : q.natDegree = 0), q = 1
⊢ q.natDegree ≠ 0

Tactic:
contrapose hq
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hpq : p %ₘ q = 0
hq : q.natDegree = 0
⊢ q = 1

Tactic:
eq_one_of_monic_natDegree_zero hmq hq

Premises used: Polynomial.eq_one_of_monic_natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hpq : p %ₘ q = 0
hq : q.natDegree = 0
⊢ q = 1

Tactic:
exact eq_one_of_monic_natDegree_zero hmq hq

Premises used: Polynomial.eq_one_of_monic_natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
⊢ Nontrivial R

Tactic:
haveI := Nontrivial.of_polynomial_ne hpq
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
this : Nontrivial R
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)

Premises used: Polynomial.degree_modByMonic_lt, Polynomial.natDegree_lt_natDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
this : Nontrivial R
⊢ (p %ₘ q).natDegree < q.natDegree

Tactic:
exact natDegree_lt_natDegree hpq (degree_modByMonic_lt p hmq)

Premises used: Polynomial.degree_modByMonic_lt, Polynomial.natDegree_lt_natDegree
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ 0 %ₘ p = 0

Tactic:
grind [modByMonic, divModByMonicAux]

Premises used: Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ 0 /ₘ p = 0

Tactic:
grind [divByMonic, divModByMonicAux]

Premises used: Polynomial.divByMonic, Polynomial.divModByMonicAux
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic.{u} (R := R) 0
⊢ Subsingleton R

Tactic:
haveI := monic_zero_iff_subsingleton.mp h
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
this_1 : DecidableEq R := Classical.decEq R
h : Monic.{u} (R := R) 0
this : Subsingleton R
⊢ p %ₘ 0 = p

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 0
unfold :
  (if h : Monic.{u} (R := R) 0 then
      (if h_1 : degree.{u} (R := R) 0 ≤ 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 - natDegree.{u} (R := R) 0));
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p
⊢ p %ₘ 0 = p

Tactic:
unfold modByMonic divModByMonicAux

Premises used: Polynomial.divModByMonicAux, Polynomial.modByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 0
rw rw₁ : p = p
⊢ (if h : Monic.{u} (R := R) 0 then
      (if h_1 : degree.{u} (R := R) 0 ≤ 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 - natDegree.{u} (R := R) 0));
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    p

Tactic:
rw [dif_neg h]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
this_1 : DecidableEq R := Classical.decEq R
h : Monic.{u} (R := R) 0
this : Subsingleton R
⊢ p /ₘ 0 = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 0
unfold :
  Eq.{u + 1} (α := R[X])
    (if h : Monic.{u} (R := R) 0 then
      (if h_1 : degree.{u} (R := R) 0 ≤ 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 - natDegree.{u} (R := R) 0));
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0)
    0
⊢ p /ₘ 0 = 0

Tactic:
unfold divByMonic divModByMonicAux

Premises used: Polynomial.divByMonic, Polynomial.divModByMonicAux
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 0
rw rw₁ : Eq.{u + 1} (α := R[X]) 0 0
⊢ Eq.{u + 1} (α := R[X])
    (if h : Monic.{u} (R := R) 0 then
      (if h_1 : degree.{u} (R := R) 0 ≤ 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 - natDegree.{u} (R := R) 0));
          have _wf := ⋯;
          have dm := (p - 0 * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0)
    0

Tactic:
rw [dif_neg h]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
q p : R[X]
hq : ¬q.Monic
⊢ p /ₘ q = 0

Tactic:
dif_neg hq

Premises used: Polynomial.divByMonic, dif_neg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
q p : R[X]
hq : ¬q.Monic
⊢ p %ₘ q = p

Tactic:
dif_neg hq

Premises used: dif_neg, Polynomial.modByMonic
-- 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
⊢ ¬q.degree ≤ p.degree

Tactic:
have : ¬degree q ≤ degree p := not_le_of_gt h
-- 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 :
  (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
⊢ p %ₘ q = p

Tactic:
unfold modByMonic divModByMonicAux

Premises used: Polynomial.divModByMonicAux, Polynomial.modByMonic
-- 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 :
  (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
⊢ (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

Tactic:
dsimp
-- 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
rw :
  (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 =
    p
rw₁ rw₂ : (0, p).2 = p
⊢ (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

Tactic:
rw [dif_pos hq, if_neg (mt And.left this)]

Premises used: mt, dif_pos, And.left, if_neg