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]
inst_1 : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ 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
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)).1 =
  0
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)).1 =
    0
⊢ 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
have rw₁ : Eq (α := R[X]) (0, p).1 0
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 = 0
have have : ∀ (this : ¬q.degree ≤ p.degree), p /ₘ q = 0
Tactic: classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold divByMonic 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 = 0
⊢ p /ₘ q = 0
have have₃ : ∀ (this : ¬q.degree ≤ p.degree),
  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 := sorry;
          have dm := (p - q * z).divModByMonicAux sorry;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0)
    0
Tactic: classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold divByMonic 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 = 0
have₃ have₄ :
  ∀ (this : ¬q.degree ≤ p.degree),
    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
have have₅ : ∀ (this : ¬q.degree ≤ p.degree),
  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
                  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)).1
    else 0)
    0
Tactic: classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold divByMonic 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
h : q.degree ≤ p.degree
⊢ q.degree + (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]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
⊢ p /ₘ q ≠ 0
have rwa : ¬p /ₘ q = 0
Tactic: rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
rwa : ¬p /ₘ q = 0
⊢ p /ₘ q ≠ 0
have rwa₁ : ¬p.degree < q.degree
Tactic: rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
⊢ q.degree + (p /ₘ q).degree = p.degree
have hdiv0 : p /ₘ q ≠ 0
Tactic: have hdiv0 : p /ₘ q ≠ 0 := by rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
have rwa : 1 * (p /ₘ q).leadingCoeff ≠ 0
Tactic: rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
rwa : 1 * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
have rwa₁ : (p /ₘ q).leadingCoeff ≠ 0
Tactic: rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
rwa : 1 * (p /ₘ q).leadingCoeff ≠ 0
rwa₁ : (p /ₘ q).leadingCoeff ≠ 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
have rwa₂ : ¬(p /ₘ q).leadingCoeff = 0
Tactic: rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
rwa : 1 * (p /ₘ q).leadingCoeff ≠ 0
rwa₁ : (p /ₘ q).leadingCoeff ≠ 0
rwa₂ : ¬(p /ₘ q).leadingCoeff = 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
have rwa₃ : ¬p /ₘ q = 0
Tactic: rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
⊢ q.degree + (p /ₘ q).degree = p.degree
have hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
Tactic: have hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0 := by
    rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree ≤ (q * (p /ₘ q)).degree
have rw : q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree
Tactic: rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
            Nat.cast_add, Nat.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
h_1 : Nontrivial R
hdiv0 : p /ₘ q ≠ 0
hlc : q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0
⊢ q.degree + (p /ₘ q).degree = p.degree
have hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
Tactic: have hmod : degree (p %ₘ q) < degree (q * (p /ₘ q)) :=
    calc
      degree (p %ₘ q) < degree q := degree_modByMonic_lt _ hq
      _ ≤ _ := by
        rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
            Nat.cast_add, Nat.cast_le]
        exact Nat.le_add_right _ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.degree
have this₁ : Nontrivial R
Tactic: haveI := Nontrivial.of_polynomial_ne hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
this_1 : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : q.degree ≤ p.degree
this : Nontrivial R
⊢ (p /ₘ q).degree ≤ p.degree
have rw : (↑(p /ₘ q).natDegree : WithBot ℕ) ≤
  HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(p /ₘ q).natDegree : WithBot ℕ)
Tactic: rw [← degree_add_divByMonic hq h, degree_eq_natDegree hq.ne_zero,
          degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 (not_lt.2 h))]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
h : ¬q.degree ≤ p.degree
⊢ (p /ₘ q).degree ≤ p.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)).1
    else 0) ≤
  p.degree
Tactic: unfold divByMonic divModByMonicAux
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree
have this₁ : Nontrivial R
Tactic: haveI := Nontrivial.of_polynomial_ne hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this_1 : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree
have rw : degree.{u} (R := R) 0 < (↑p.natDegree : WithBot ℕ)
Tactic: rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
⊢ (p /ₘ q).degree < p.degree
have this₁ : Nontrivial R
Tactic: haveI := Nontrivial.of_polynomial_ne hp0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this_1 : DecidableEq R := Classical.decEq R
hq : q.Monic
hpq : ¬p.degree < q.degree
this : Nontrivial R
⊢ (p /ₘ q).degree < p.degree
have rw : (↑(p /ₘ q).natDegree : WithBot ℕ) <
  HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(p /ₘ q).natDegree : WithBot ℕ)
Tactic: rw [← degree_add_divByMonic hq (not_lt.1 hpq), degree_eq_natDegree hq.ne_zero,
        degree_eq_natDegree (mt (divByMonic_eq_zero_iff hq).1 hpq)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
⊢ (p /ₘ q).degree < p.degree
have rwa : degree.{u} (R := R) 0 < p.degree
Tactic: rwa [divByMonic_eq_of_not_monic _ hq, degree_zero, bot_lt_iff_ne_bot, degree_ne_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
rwa : degree.{u} (R := R) 0 < p.degree
⊢ (p /ₘ q).degree < p.degree
have rwa₁ : ⊥ < p.degree
Tactic: rwa [divByMonic_eq_of_not_monic _ hq, degree_zero, bot_lt_iff_ne_bot, degree_ne_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hp0 : p ≠ 0
h0q : 0 < q.degree
this : DecidableEq R := Classical.decEq R
hq : ¬q.Monic
rwa : degree.{u} (R := R) 0 < p.degree
rwa₁ : ⊥ < p.degree
⊢ (p /ₘ q).degree < p.degree
have rwa₂ : p.degree ≠ ⊥
Tactic: rwa [divByMonic_eq_of_not_monic _ hq, degree_zero, bot_lt_iff_ne_bot, degree_ne_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have pos : ∀ (hfg : f /ₘ g = 0), (f /ₘ g).natDegree = f.natDegree - g.natDegree
Tactic: by_cases hfg : f /ₘ g = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
pos : ∀ (hfg : f /ₘ g = 0), (f /ₘ g).natDegree = f.natDegree - g.natDegree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have neg : ∀ (hfg : ¬f /ₘ g = 0), (f /ₘ g).natDegree = f.natDegree - g.natDegree
Tactic: by_cases hfg : f /ₘ g = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have pos : 0 = f.natDegree - g.natDegree
Tactic: rw [hfg, natDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : f /ₘ g = 0
⊢ 0 = f.natDegree - g.natDegree
have hfg₁ : f.degree < g.degree
Tactic: rw [divByMonic_eq_zero_iff hg] at hfg
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : f.degree < g.degree
⊢ 0 = f.natDegree - g.natDegree
have pos : Eq (α := ℕ) 0 0
Tactic: rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have hgf₁ : ¬f.degree < g.degree
Tactic: rw [divByMonic_eq_zero_iff hg] at hgf
Cleared hypotheses: hgf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : ¬f.degree < g.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have hgf₁ : g.degree ≤ f.degree
Tactic: push Not at hgf
Cleared hypotheses: hgf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have this : g.degree + (f /ₘ g).degree = f.degree
Tactic: have := degree_add_divByMonic hg hgf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ False
have apply : f /ₘ g = 0
Tactic: apply hfg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
⊢ f /ₘ g = 0
have rw : 0 /ₘ g = 0
Tactic: rw [hf, zero_divByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f = 0
rw : 0 /ₘ g = 0
⊢ f /ₘ g = 0
have rw₁ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [hf, zero_divByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have hf : f ≠ 0
Tactic: have hf : f ≠ 0 := by
    intro hf
    apply hfg
    rw [hf, zero_divByMonic]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.degree + (f /ₘ g).degree = f.degree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have this₁ : g.natDegree + (f /ₘ g).natDegree = f.natDegree
Tactic: rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
    ← Nat.cast_add, Nat.cast_inj] at this
Cleared hypotheses: this, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have neg : (f /ₘ g).natDegree = g.natDegree + (f /ₘ g).natDegree - g.natDegree
Tactic: rw [← this, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
hgf : g.degree ≤ f.degree
this : g.natDegree + (f /ₘ g).natDegree = f.natDegree
hf : f ≠ 0
neg : (f /ₘ g).natDegree = g.natDegree + (f /ₘ g).natDegree - g.natDegree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree
have neg₁ : (f /ₘ g).natDegree = (f /ₘ g).natDegree
Tactic: rw [← this, add_tsub_cancel_left]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
⊢ f /ₘ g = q ∧ f %ₘ g = r
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = 0
have rw : r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))
Tactic: rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
⊢ f /ₘ g = q ∧ f %ₘ g = r
have h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
Tactic: have h₁ : r - f %ₘ g = -g * (q - f /ₘ g) :=
    eq_of_sub_eq_zero
      (by
        rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]
        simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
⊢ f /ₘ g = q ∧ f %ₘ g = r
have h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
Tactic: have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (hypothesis)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
⊢ f /ₘ g = q ∧ f %ₘ g = r
have h₄ : (r - f %ₘ g).degree < g.degree
Tactic: have h₄ : degree (r - f %ₘ g) < degree g :=
    calc
      degree (r - f %ₘ g) ≤ max (degree r) (degree (f %ₘ g)) := degree_sub_le _ _
      _ < degree g := max_lt_iff.2 ⟨h.2, degree_modByMonic_lt _ hg⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree ≤ g.degree + (q - f /ₘ g).degree
have rw : (↑g.natDegree : WithBot ℕ) ≤ HAdd.hAdd (α := WithBot ℕ) (↑g.natDegree : WithBot ℕ) (↑(q - f /ₘ g).natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ (↑g.natDegree : WithBot ℕ) ≤
    HAdd.hAdd (α := WithBot ℕ) (↑g.natDegree : WithBot ℕ) (↑(q - f /ₘ g).natDegree : WithBot ℕ)
have norm_cast : g.natDegree ≤ g.natDegree + (q - f /ₘ g).natDegree
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
f g q r : R[X]
hg : g.Monic
h : r + g * q = f ∧ r.degree < g.degree
h_1 : Nontrivial R
h₁ : r - f %ₘ g = -g * (q - f /ₘ g)
h₂ : (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree
h₄ : (r - f %ₘ g).degree < g.degree
hqf : ¬q - f /ₘ g = 0
⊢ g.degree + (q - f /ₘ g).degree = (r - f %ₘ g).degree
have rw : g.leadingCoeff * (q - f /ₘ g).leadingCoeff ≠ 0
Tactic: rw [h₂, degree_mul']