awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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)
⊢ 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
have rw₂ : p.leadingCoeff = p.leadingCoeff
Tactic: rw [leadingCoeff_monic_mul hq, leadingCoeff_mul_X_pow, leadingCoeff_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
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).degree < q.degree
have _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
Tactic: have _wf := div_wf_lemma ⟨h.1, h.2⟩ hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
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).degree < q.degree
have 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
Tactic: have :=
        degree_modByMonic_lt (p - q * (C (leadingCoeff p) * X ^ (natDegree p - natDegree q))) hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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), (p %ₘ q).degree < q.degree
have 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 := sorry;
            have dm := (p - q * z).divModByMonicAux sorry;
            (z + dm.1, dm.2)
          else (0, p)).2
      else p) <
    q.degree
Tactic: unfold modByMonic divModByMonicAux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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),
    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
have 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
                    sorry).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
                  sorry).2)
          else (0, p)).2
      else p) <
    q.degree
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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),
    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
have rw : ∀ (h : ¬q.degree ≤ p.degree), (0, p).2.degree < q.degree
Tactic: rw [dif_pos hq, if_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ (p %ₘ q).degree < q.degree
have 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 := sorry;
          have dm := (p - q * z).divModByMonicAux sorry;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) <
  q.degree
Tactic: unfold modByMonic divModByMonicAux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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)
      (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
have 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
                  sorry).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
                sorry).2)
        else (0, p)).2
    else p) <
  q.degree
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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)
      (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
have rw : degree.{u} (R := R) (0, 0).2 < q.degree
Tactic: rw [dif_pos hq, if_neg h, Classical.not_not.1 hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
⊢ (p %ₘ q).natDegree < q.natDegree
have pos : ∀ (hpq : p %ₘ q = 0), (p %ₘ q).natDegree < q.natDegree
Tactic: by_cases hpq : p %ₘ q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ (p %ₘ q).natDegree < q.natDegree
have neg : ∀ (hpq : ¬p %ₘ q = 0), (p %ₘ q).natDegree < q.natDegree
Tactic: by_cases hpq : p %ₘ q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree
have pos : q.natDegree ≠ 0
Tactic: rw [hpq, natDegree_zero, Nat.pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : p %ₘ q = 0
⊢ q.natDegree ≠ 0
have pos : ∀ (hq : q.natDegree = 0), q = 1
Tactic: contrapose hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hmq : q.Monic
hq : q ≠ 1
hpq : ¬p %ₘ q = 0
⊢ (p %ₘ q).natDegree < q.natDegree
have this : Nontrivial R
Tactic: haveI := Nontrivial.of_polynomial_ne hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic.{u} (R := R) 0
⊢ p %ₘ 0 = p
have this₁ : Subsingleton R
Tactic: haveI := monic_zero_iff_subsingleton.mp h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 0
⊢ p %ₘ 0 = p
have 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 := sorry;
        have dm := (p - 0 * z).divModByMonicAux sorry;
        (z + dm.1, dm.2)
      else (0, p)).2
  else p) =
  p
Tactic: unfold modByMonic divModByMonicAux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 0
⊢ (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
have rw : p = p
Tactic: rw [dif_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : Monic.{u} (R := R) 0
⊢ p /ₘ 0 = 0
have this₁ : Subsingleton R
Tactic: haveI := monic_zero_iff_subsingleton.mp h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 0
⊢ p /ₘ 0 = 0
have 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 := sorry;
        have dm := (p - 0 * z).divModByMonicAux sorry;
        (z + dm.1, dm.2)
      else (0, p)).1
  else 0)
  0
Tactic: unfold divByMonic divModByMonicAux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
this : DecidableEq R := Classical.decEq R
h : ¬Monic.{u} (R := R) 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
have rw : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [dif_neg h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
inst_1 : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p %ₘ q = p
have this : ¬q.degree ≤ p.degree
Tactic: have : ¬degree q ≤ degree p := not_le_of_gt h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ p %ₘ q = p
have 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 := sorry;
        have dm := (p - q * z).divModByMonicAux sorry;
        (z + dm.1, dm.2)
      else (0, p)).2
  else p) =
  p
Tactic: unfold modByMonic divModByMonicAux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ (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 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
                sorry).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
              sorry).2)
      else (0, p)).2
  else p) =
  p
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ (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
have 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
              sorry).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
            sorry).2)
    else (0, p)).2 =
  p
Tactic: rw [dif_pos hq, if_neg (mt And.left this)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ (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
have rw₁ : (0, p).2 = p
Tactic: rw [dif_pos hq, if_neg (mt And.left this)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
inst_1 : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p %ₘ q = p
have have : ∀ (this : ¬q.degree ≤ p.degree), 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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ 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 := sorry;
          have dm := (p - q * z).divModByMonicAux sorry;
          (z + dm.1, dm.2)
        else (0, p)).2
    else p) =
    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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ p %ₘ q = 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
                  sorry).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
                sorry).2)
        else (0, p)).2
    else p) =
    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)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
⊢ (p %ₘ q).degree ≤ q.degree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ (p %ₘ q).degree ≤ p.degree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
⊢ (p %ₘ q).degree ≤ p.degree
have pos : ∀ (hq : q.Monic), (p %ₘ q).degree ≤ p.degree
Tactic: by_cases hq : q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
pos : ∀ (hq : q.Monic), (p %ₘ q).degree ≤ p.degree
⊢ (p %ₘ q).degree ≤ p.degree
have neg : ∀ (hq : ¬q.Monic), (p %ₘ q).degree ≤ p.degree
Tactic: by_cases hq : q.Monic
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : q.Monic
⊢ (p %ₘ q).degree ≤ p.degree
have pos : p.degree < q.degree → (p %ₘ q).degree ≤ p.degree
Tactic: cases lt_or_ge (degree p) (degree q)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
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
⊢ (p %ₘ q).degree ≤ p.degree
have pos₁ : q.degree ≤ p.degree → (p %ₘ q).degree ≤ p.degree
Tactic: cases lt_or_ge (degree p) (degree q)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : q.Monic
h_1 : p.degree < q.degree
⊢ (p %ₘ q).degree ≤ p.degree
have pos : p.degree ≤ p.degree
Tactic: rw [(modByMonic_eq_self_iff hq).mpr ‹_›]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : Nontrivial R
hq : ¬q.Monic
⊢ (p %ₘ q).degree ≤ p.degree
have neg : p.degree ≤ p.degree
Tactic: rw [modByMonic_eq_of_not_monic p hq]