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
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
rw₁ rw₂ : Eq (α := R[X]) (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

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

Premises used: mt, dif_pos, And.left, if_neg
-- 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 = 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
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
                    ⋯).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
⊢ 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)]

Premises used: dif_pos, Polynomial.divByMonic, Polynomial.divModByMonicAux
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
hq : q.Monic
h : q.degree ≤ p.degree
⊢ 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 : q.degree ≤ p.degree
h_1 : Nontrivial R
rwa : ¬p /ₘ q = 0
rwa₁ : ¬p.degree < q.degree
rwa₂ rwa₃ rwa₄ rwa₅ : q.degree ≤ p.degree
⊢ p /ₘ q ≠ 0

Tactic:
rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]

Premises used: Polynomial.divByMonic_eq_zero_iff, Ne, not_lt
-- Module: Mathlib.Algebra.Polynomial.Div
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

Tactic:
have hdiv0 : p /ₘ q ≠ 0 := by rwa [Ne, divByMonic_eq_zero_iff hq, not_lt]
-- Module: Mathlib.Algebra.Polynomial.Div
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
rwa₃ rwa₄ rwa₅ rwa₆ : ¬p /ₘ q = 0
⊢ q.leadingCoeff * (p /ₘ q).leadingCoeff ≠ 0

Tactic:
rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]

Premises used: Ne, Iff.mp, Polynomial.Monic.def, Polynomial.leadingCoeff_eq_zero, one_mul
-- Module: Mathlib.Algebra.Polynomial.Div
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

Tactic:
have hlc : leadingCoeff q * leadingCoeff (p /ₘ q) ≠ 0 := by
    rwa [Monic.def.1 hq, one_mul, Ne, leadingCoeff_eq_zero]
-- Module: Mathlib.Algebra.Polynomial.Div
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
rw : q.natDegree ≤ q.natDegree + (p /ₘ q).natDegree
⊢ q.degree ≤ (q * (p /ₘ q)).degree

Tactic:
rw [degree_mul' hlc, degree_eq_natDegree hq.ne_zero, degree_eq_natDegree hdiv0, ←
            Nat.cast_add, Nat.cast_le]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.degree_mul', Nat.cast_add, Nat.cast_le, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
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.natDegree ≤ q.natDegree + (p /ₘ q).natDegree

Tactic:
Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Algebra.Polynomial.Div
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.natDegree ≤ q.natDegree + (p /ₘ q).natDegree

Tactic:
exact Nat.le_add_right _ _

Premises used: Nat.le_add_right
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ (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 _ _
-- Module: Mathlib.Algebra.Polynomial.Div
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
hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ q.degree + (p /ₘ q).degree = (q * (p /ₘ q)).degree

Tactic:
Eq.symm (degree_mul' hlc)

Premises used: Polynomial.degree_mul', Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Div
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
hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ (q * (p /ₘ q)).degree = (p %ₘ q + q * (p /ₘ q)).degree

Tactic:
(degree_add_eq_right_of_degree_lt hmod).symm

Premises used: Polynomial.degree_add_eq_right_of_degree_lt, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Div
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
hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ (p %ₘ q + q * (p /ₘ q)).degree = p.degree

Tactic:
congr_arg _ (modByMonic_add_div _ _)

Premises used: congr_arg, Polynomial.modByMonic_add_div
-- Module: Mathlib.Algebra.Polynomial.Div
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
hmod : (p %ₘ q).degree < (q * (p /ₘ q)).degree
⊢ q.degree + (p /ₘ q).degree = p.degree

Tactic:
calc
    degree q + degree (p /ₘ q) = degree (q * (p /ₘ q)) := Eq.symm (degree_mul' hlc)
    _ = degree (p %ₘ q + q * (p /ₘ q)) := (degree_add_eq_right_of_degree_lt hmod).symm
    _ = _ := congr_arg _ (modByMonic_add_div _ _)

Premises used: HMul.hMul, Polynomial.degree_add_eq_right_of_degree_lt, Polynomial.degree, Polynomial.divByMonic, congr_arg, Polynomial.degree_mul', HAdd.hAdd, Polynomial.modByMonic, Polynomial.modByMonic_add_div, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
⊢ (p /ₘ q).degree ≤ p.degree

Tactic:
simp only [hp0, zero_divByMonic, le_refl]

Premises used: le_refl, Polynomial.zero_divByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ Nontrivial R

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0
-- Module: Mathlib.Algebra.Polynomial.Div
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
rw :
  (↑(p /ₘ q).natDegree : WithBot ℕ) ≤
    HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(p /ₘ q).natDegree : WithBot ℕ)
⊢ (p /ₘ q).degree ≤ p.degree

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))]

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, Polynomial.divByMonic_eq_zero_iff, mt, not_lt, Polynomial.degree_add_divByMonic, Iff.mp, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
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).natDegree : WithBot ℕ) ≤
    HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(p /ₘ q).natDegree : WithBot ℕ)

Tactic:
WithBot.coe_le_coe.2 (Nat.le_add_left _ _)

Premises used: Iff.mpr, WithBot.some, Nat.le_add_left, WithBot.coe_le_coe, WithBot.map₂, Option.map₂
-- Module: Mathlib.Algebra.Polynomial.Div
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).natDegree : WithBot ℕ) ≤
    HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(p /ₘ q).natDegree : WithBot ℕ)

Tactic:
exact WithBot.coe_le_coe.2 (Nat.le_add_left _ _)

Premises used: Iff.mpr, Nat.le_add_left, WithBot.coe_le_coe
-- Module: Mathlib.Algebra.Polynomial.Div
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
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)).1
      else 0) ≤
    p.degree
⊢ (p /ₘ q).degree ≤ p.degree

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]
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hq : q.Monic
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)).1
      else 0) ≤
    p.degree

Tactic:
simp [dif_pos hq, h, degree_zero, bot_le]

Premises used: dif_pos, Polynomial.degree_zero, bot_le
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ Nontrivial R

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0
-- Module: Mathlib.Algebra.Polynomial.Div
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
rw : degree.{u} (R := R) 0 < (↑p.natDegree : WithBot ℕ)
⊢ (p /ₘ q).degree < p.degree

Tactic:
rw [(divByMonic_eq_zero_iff hq).2 hpq, degree_eq_natDegree hp0]

Premises used: Iff.mpr, Polynomial.degree_eq_natDegree, Polynomial.divByMonic_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ degree.{u} (R := R) 0 < (↑p.natDegree : WithBot ℕ)

Tactic:
WithBot.bot_lt_coe _

Premises used: Multiset.foldr, Finset.fold, Polynomial.degree, WithBot.bot_lt_coe, Finset.max, Finset.sup, List.foldr, Multiset.fold
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ degree.{u} (R := R) 0 < (↑p.natDegree : WithBot ℕ)

Tactic:
exact WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ Nontrivial R

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0
-- Module: Mathlib.Algebra.Polynomial.Div
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
rw :
  (↑(p /ₘ q).natDegree : WithBot ℕ) <
    HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(p /ₘ q).natDegree : WithBot ℕ)
⊢ (p /ₘ q).degree < p.degree

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)]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.divByMonic_eq_zero_iff, mt, not_lt, Polynomial.degree_add_divByMonic, Iff.mp, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ LT.lt (α := ℕ) (↑0 : ℕ) (↑(↑q.natDegree : ℕ) : ℕ)

Tactic:
simpa [degree_eq_natDegree hq.ne_zero] using h0q

Premises used: Polynomial.degree_eq_natDegree, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
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).natDegree : WithBot ℕ) <
    HAdd.hAdd (α := WithBot ℕ) (↑q.natDegree : WithBot ℕ) (↑(p /ₘ q).natDegree : WithBot ℕ)

Tactic:
exact
        Nat.cast_lt.2
          (Nat.lt_add_of_pos_left (Nat.cast_lt.1 <|
            by simpa [degree_eq_natDegree hq.ne_zero] using h0q))

Premises used: Iff.mpr, Nat.lt_add_of_pos_left, Iff.mp, Nat.cast_lt
-- Module: Mathlib.Algebra.Polynomial.Div
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
rwa₂ : p.degree ≠ ⊥
rwa₃ rwa₄ rwa₅ rwa₆ : p ≠ 0
⊢ (p /ₘ q).degree < p.degree

Tactic:
rwa [divByMonic_eq_of_not_monic _ hq, degree_zero, bot_lt_iff_ne_bot, degree_ne_bot]

Premises used: Polynomial.divByMonic_eq_of_not_monic, bot_lt_iff_ne_bot, Polynomial.degree_zero, Polynomial.degree_ne_bot
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
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
neg : ∀ (hfg : ¬f /ₘ g = 0), (f /ₘ g).natDegree = f.natDegree - g.natDegree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
by_cases hfg : f /ₘ g = 0
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : f /ₘ g = 0
pos : 0 = f.natDegree - g.natDegree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [hfg, natDegree_zero]

Premises used: Polynomial.natDegree_zero
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : f /ₘ g = 0
⊢ f.degree < g.degree

Tactic:
rw [divByMonic_eq_zero_iff hg] at hfg

Premises used: Polynomial.divByMonic_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : f.degree < g.degree
pos pos₁ : Eq (α := ℕ) 0 0
⊢ 0 = f.natDegree - g.natDegree

Tactic:
rw [tsub_eq_zero_iff_le.mpr (natDegree_le_natDegree <| le_of_lt hfg)]

Premises used: Iff.mpr, Polynomial.natDegree_le_natDegree, le_of_lt, tsub_eq_zero_iff_le
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg : ¬f /ₘ g = 0
⊢ ¬f /ₘ g = 0

Tactic:
have hgf := hfg
-- Module: Mathlib.Algebra.Polynomial.Div
Goal:
R : Type u
inst : Ring R
f g : R[X]
hg : g.Monic
h : Nontrivial R
hfg hgf : ¬f /ₘ g = 0
⊢ ¬f.degree < g.degree

Tactic:
rw [divByMonic_eq_zero_iff hg] at hgf

Premises used: Polynomial.divByMonic_eq_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ g.degree ≤ f.degree

Tactic:
push Not at hgf

Premises used: Not
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ g.degree + (f /ₘ g).degree = f.degree

Tactic:
have := degree_add_divByMonic hg hgf
-- Module: Mathlib.Algebra.Polynomial.Div
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
apply : f /ₘ g = 0
⊢ False

Tactic:
apply hfg
-- Module: Mathlib.Algebra.Polynomial.Div
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
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) 0 0
⊢ f /ₘ g = 0

Tactic:
rw [hf, zero_divByMonic]

Premises used: Polynomial.zero_divByMonic
-- Module: Mathlib.Algebra.Polynomial.Div
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 ≠ 0

Tactic:
have hf : f ≠ 0 := by
    intro hf
    apply hfg
    rw [hf, zero_divByMonic]
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ 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

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_inj, Nat.cast_add, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
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
this₁ : g.natDegree + (f /ₘ g).natDegree = f.natDegree
⊢ f ≠ 0

Tactic:
rw [degree_eq_natDegree hf, degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hfg,
    ← Nat.cast_add, Nat.cast_inj] at this

Premises used: Polynomial.degree_eq_natDegree, Nat.cast_inj, Nat.cast_add, Polynomial.Monic.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Div
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
neg₁ neg₂ : (f /ₘ g).natDegree = (f /ₘ g).natDegree
⊢ (f /ₘ g).natDegree = f.natDegree - g.natDegree

Tactic:
rw [← this, add_tsub_cancel_left]

Premises used: add_tsub_cancel_left
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Algebra.Polynomial.Div
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
rw : r - f %ₘ g - -g * (q - f /ₘ g) = r + g * q - (f %ₘ g + g * (f /ₘ g))
⊢ r - f %ₘ g - -g * (q - f /ₘ g) = 0

Tactic:
rw [← sub_eq_zero_of_eq (h.1.trans (modByMonic_add_div f g).symm)]

Premises used: sub_eq_zero_of_eq, And.left, Polynomial.modByMonic_add_div, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Div
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) = r + g * q - (f %ₘ g + g * (f /ₘ g))

Tactic:
simp [mul_add, sub_eq_add_neg, add_comm, add_left_comm, add_assoc]

Premises used: add_left_comm, add_assoc, sub_eq_add_neg, add_comm, mul_add
-- Module: Mathlib.Algebra.Polynomial.Div
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)

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])
-- Module: Mathlib.Algebra.Polynomial.Div
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)
⊢ (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree

Tactic:
simp [h₁]
-- Module: Mathlib.Algebra.Polynomial.Div
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)
⊢ (r - f %ₘ g).degree = (g * (q - f /ₘ g)).degree

Tactic:
have h₂ : degree (r - f %ₘ g) = degree (g * (q - f /ₘ g)) := by simp [h₁]
-- Module: Mathlib.Algebra.Polynomial.Div
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
⊢ (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⟩
-- Module: Mathlib.Algebra.Polynomial.Div
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
rw :
  (↑g.natDegree : WithBot ℕ) ≤
    HAdd.hAdd (α := WithBot ℕ) (↑g.natDegree : WithBot ℕ) (↑(q - f /ₘ g).natDegree : WithBot ℕ)
⊢ g.degree ≤ g.degree + (q - f /ₘ g).degree

Tactic:
rw [degree_eq_natDegree hg.ne_zero, degree_eq_natDegree hqf]

Premises used: Polynomial.degree_eq_natDegree, Polynomial.Monic.ne_zero