awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
mp :
  X i ∣
    X i * p.divMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) +
      (X i * p.modMonomial (Finsupp.single i 1) * q.divMonomial (Finsupp.single i 1) +
        HMul.hMul (α := MvPolynomial σ R) (X i) (X i) * p.divMonomial (Finsupp.single i 1) *
          q.divMonomial (Finsupp.single i 1))
⊢ X i ∣
    X i * p.divMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) +
      (p.modMonomial (Finsupp.single i 1) * (X i * q.divMonomial (Finsupp.single i 1)) +
        X i * p.divMonomial (Finsupp.single i 1) * (X i * q.divMonomial (Finsupp.single i 1)))

Tactic:
simp only [← mul_assoc, mul_comm _ (X i)]

Premises used: mul_assoc, MvPolynomial.X, mul_comm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
mp :
  X i ∣
    X i *
      (p.divMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) +
        (p.modMonomial (Finsupp.single i 1) * q.divMonomial (Finsupp.single i 1) +
          X i * (p.divMonomial (Finsupp.single i 1) * q.divMonomial (Finsupp.single i 1))))
⊢ X i ∣
    X i * p.divMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) +
      (X i * p.modMonomial (Finsupp.single i 1) * q.divMonomial (Finsupp.single i 1) +
        HMul.hMul (α := MvPolynomial σ R) (X i) (X i) * p.divMonomial (Finsupp.single i 1) *
          q.divMonomial (Finsupp.single i 1))

Tactic:
simp only [mul_assoc, ← mul_add (X i)]

Premises used: mul_assoc, MvPolynomial.X, mul_add
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣
    X i *
      (p.divMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) +
        (p.modMonomial (Finsupp.single i 1) * q.divMonomial (Finsupp.single i 1) +
          X i * (p.divMonomial (Finsupp.single i 1) * q.divMonomial (Finsupp.single i 1))))

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ p
⊢ X i ∣ p * q

Tactic:
dvd_mul_of_dvd_left h q

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ p
⊢ X i ∣ p * q

Tactic:
exact dvd_mul_of_dvd_left h q

Premises used: dvd_mul_of_dvd_left
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ q
⊢ X i ∣ p * q

Tactic:
dvd_mul_of_dvd_right h p

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ q
⊢ X i ∣ p * q

Tactic:
exact dvd_mul_of_dvd_right h p

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
inst_1 : IsCancelMulZero R
inst_2 : Nontrivial R
⊢ Prime (M := MvPolynomial σ R) (X i)

Tactic:
⟨X_ne_zero i, ?_, fun p q ↦ X_dvd_mul_iff.mp⟩

Premises used: Prime, MvPolynomial.X_dvd_mul_iff, And.intro, Iff.mp, MvPolynomial.X_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
inst_1 : IsCancelMulZero R
inst_2 : Nontrivial R
refine : ¬IsUnit (M := MvPolynomial σ R) (X i)
⊢ Prime (M := MvPolynomial σ R) (X i)

Tactic:
refine ⟨X_ne_zero i, ?_, fun p q ↦ X_dvd_mul_iff.mp⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
inst_1 : IsCancelMulZero R
inst_2 : Nontrivial R
h : IsUnit (M := MvPolynomial σ R) (X i)
⊢ ∃ (b : MvPolynomial σ R), X i * b = 1 ∧ b * X i = 1

Tactic:
rw [isUnit_iff_exists] at h

Premises used: isUnit_iff_exists
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
inst_1 : IsCancelMulZero R
inst_2 : Nontrivial R
h : ∃ (b : MvPolynomial σ R), X i * b = 1 ∧ b * X i = 1
rcases : ∀ (u : MvPolynomial σ R) (hu : X i * u = 1), False
⊢ False

Tactic:
rcases h with ⟨u, hu, -⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
inst_1 : IsCancelMulZero R
inst_2 : Nontrivial R
u : MvPolynomial σ R
hu : X i * u = 1
⊢ Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) (X i * u) : R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) 1 : R)

Tactic:
apply_fun constantCoeff at hu

Premises used: MvPolynomial.constantCoeff
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
inst_1 : IsCancelMulZero R
inst_2 : Nontrivial R
u : MvPolynomial σ R
hu :
  Eq.{u_3 + 1} (α := R) ((constantCoeff : (a : MvPolynomial σ R) → R) (X i * u) : R)
    ((constantCoeff : (a : MvPolynomial σ R) → R) 1 : R)
⊢ False

Tactic:
simp at hu
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
mp : p ∣ X i * q → p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
mpr : p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q → p ∣ X i * q
⊢ p ∣ X i * q ↔ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
⊢ X i ∣ p ∨ X i ∣ r

Tactic:
simp [← X_dvd_mul_iff, ← hp]

Premises used: MvPolynomial.X_dvd_mul_iff
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
⊢ X i ∣ p ∨ X i ∣ r

Tactic:
have : X i ∣ p ∨ X i ∣ r := by simp [← X_dvd_mul_iff, ← hp]
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
mp : X i ∣ r → p ∣ q
mp₁ : X i ∣ p → X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
apply this.symm.imp

Premises used: Or.symm, Or.imp
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * (X i * r)
this : X i ∣ p ∨ X i ∣ X i * r
rw : X i * q = X i * (p * r)
rw₁ : p * (X i * r) = X i * (p * r)
rw₂ rw₃ : X i * (p * r) = X i * (p * r)
⊢ q = p * r

Tactic:
rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]

Premises used: MvPolynomial.X_mul_cancel_left_iff, mul_left_comm
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * (X i * r)
this : X i ∣ p ∨ X i ∣ X i * r
mp : ∀ (hp : X i * (p * r) = p * (X i * r)), p ∣ p * r
⊢ p ∣ q

Tactic:
obtain rfl : q = p * r := by rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]

Premises used: rfl
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
this : X i ∣ p ∨ X i ∣ X i * r
hp : X i * (p * r) = p * (X i * r)
⊢ p ∣ p * r

Tactic:
dvd_mul_right p r

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
this : X i ∣ p ∨ X i ∣ X i * r
hp : X i * (p * r) = p * (X i * r)
⊢ p ∣ p * r

Tactic:
exact dvd_mul_right p r

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : X i ∣ p
⊢ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
⟨hip, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : X i ∣ p
mp : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
refine ⟨hip, ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : X i ∣ p
⊢ p.modMonomial (Finsupp.single i 1) = 0

Tactic:
rw [X_dvd_iff_modMonomial_eq_zero] at hip

Premises used: MvPolynomial.X_dvd_iff_modMonomial_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
⊢ q = p.divMonomial (Finsupp.single i 1) * r

Tactic:
rw [← p.modMonomial_add_divMonomial_single i, hip,
        zero_add, mul_assoc, X_mul_cancel_left_iff] at hp

Premises used: mul_assoc, MvPolynomial.X_mul_cancel_left_iff, zero_add, MvPolynomial.modMonomial_add_divMonomial_single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
hp₁ : q = p.divMonomial (Finsupp.single i 1) * r
⊢ X i ∣ p ∨ X i ∣ r

Tactic:
rw [← p.modMonomial_add_divMonomial_single i, hip,
        zero_add, mul_assoc, X_mul_cancel_left_iff] at hp

Premises used: mul_assoc, MvPolynomial.X_mul_cancel_left_iff, zero_add, MvPolynomial.modMonomial_add_divMonomial_single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
hp₁ : q = p.divMonomial (Finsupp.single i 1) * r
this₁ : X i ∣ p ∨ X i ∣ r
⊢ p.modMonomial (Finsupp.single i 1) = 0

Tactic:
rw [← p.modMonomial_add_divMonomial_single i, hip,
        zero_add, mul_assoc, X_mul_cancel_left_iff] at hp

Premises used: mul_assoc, MvPolynomial.X_mul_cancel_left_iff, zero_add, MvPolynomial.modMonomial_add_divMonomial_single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
r : MvPolynomial σ R
hp : q = p.divMonomial (Finsupp.single i 1) * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
w : MvPolynomial σ R
h : q = p.divMonomial (Finsupp.single i 1) * r
⊢ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
use r
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hp : p ∣ q
⊢ p ∣ X i * q

Tactic:
dvd_mul_of_dvd_right hp (X i)

Premises used: dvd_mul_of_dvd_right, MvPolynomial.X
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hp : p ∣ q
⊢ p ∣ X i * q

Tactic:
exact dvd_mul_of_dvd_right hp (X i)

Premises used: dvd_mul_of_dvd_right, MvPolynomial.X
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
this : p = X i * p.divMonomial (Finsupp.single i 1)
rw : X i * p.divMonomial (Finsupp.single i 1) ∣ X i * q
⊢ p ∣ X i * q

Tactic:
rw [this]
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
this : p = X i * p.divMonomial (Finsupp.single i 1)
⊢ X i * p.divMonomial (Finsupp.single i 1) ∣ X i * q

Tactic:
mul_dvd_mul_left (X i) hq

Premises used: MvPolynomial.X, mul_dvd_mul_left
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
this : p = X i * p.divMonomial (Finsupp.single i 1)
⊢ X i * p.divMonomial (Finsupp.single i 1) ∣ X i * q

Tactic:
exact mul_dvd_mul_left (X i) hq

Premises used: MvPolynomial.X, mul_dvd_mul_left
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
mpr : p = X i * p.divMonomial (Finsupp.single i 1)
⊢ p ∣ X i * q

Tactic:
suffices p = X i * p.divMonomial (Finsupp.single i 1) by
        rw [this]
        exact mul_dvd_mul_left (X i) hq
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
rw :
  p.modMonomial (Finsupp.single i 1) +
    (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * p.divMonomial (Finsupp.single i 1)
| p

Tactic:
rw [← p.modMonomial_add_divMonomial (Finsupp.single i 1)]

Premises used: MvPolynomial.modMonomial_add_divMonomial, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
mpr :
  p.modMonomial (Finsupp.single i 1) +
      (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * p.divMonomial (Finsupp.single i 1) =
    X i * p.divMonomial (Finsupp.single i 1)
⊢ p = X i * p.divMonomial (Finsupp.single i 1)

Tactic:
conv_lhs => rw [← p.modMonomial_add_divMonomial (Finsupp.single i 1)]

Premises used: MvPolynomial.modMonomial_add_divMonomial, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p.modMonomial (Finsupp.single i 1) +
      (monomial (Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * p.divMonomial (Finsupp.single i 1) =
    X i * p.divMonomial (Finsupp.single i 1)

Tactic:
simpa only [← C_mul_X_eq_monomial, C_1, one_mul, add_eq_right,
        ← X_dvd_iff_modMonomial_eq_zero]

Premises used: MvPolynomial.C_mul_X_eq_monomial, MvPolynomial.C_1, MvPolynomial.X_dvd_iff_modMonomial_eq_zero, add_eq_right, one_mul
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
inl :
  ∀ (hR : Subsingleton R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
inr :
  ∀ (hR : Nontrivial R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Subsingleton R
inl : ∃ (m : σ →₀ ℕ), m ≤ n
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
simp only [Subsingleton.elim _ p, dvd_refl, and_self, and_true, exists_const, true_iff]

Premises used: and_true, and_self, true_iff, exists_const, Subsingleton.elim, dvd_refl
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Subsingleton R
⊢ ∃ (m : σ →₀ ℕ), m ≤ n

Tactic:
⟨n, le_refl n⟩

Premises used: le_refl, Exists.intro
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Subsingleton R
⊢ ∃ (m : σ →₀ ℕ), m ≤ n

Tactic:
refine ⟨n, le_refl n⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
inr :
  ∀ (d : ℕ) (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
suffices ∀ (d) (n : σ →₀ ℕ) (hd : n.degree = d) (p q : MvPolynomial σ R),
    p ∣ monomial n 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = monomial m 1 * r from this n.degree n rfl p q
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
n : σ →₀ ℕ
hn : Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n : ℕ) (0 : ℕ)
p : MvPolynomial σ R
inr :
  ∀ (hn : n = 0) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∀ (q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
rw [Finsupp.degree_eq_zero_iff] at hn

Premises used: Finsupp.degree_eq_zero_iff
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
n : σ →₀ ℕ
hn : n = 0
p : MvPolynomial σ R
⊢ ∀ (q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
simp only [hn, monomial_zero', C_1, one_mul, nonpos_iff_eq_zero, exists_and_left,
      exists_eq_left, exists_eq_right', implies_true]

Premises used: exists_eq_right', MvPolynomial.C_1, exists_and_left, exists_eq_left, MvPolynomial.monomial_zero', implies_true, one_mul, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
⟨fun hp ↦ ?_, fun ⟨m, r, hmn, hrq, hp⟩ ↦ ?_⟩

Premises used: Dvd.dvd, _private.0.MvPolynomial.dvd_monomial_mul_iff_exists.match_5, HMul.hMul, MvPolynomial.monomial, Iff.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
inr :
  ∀ (hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q),
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
inr₁ :
  (∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r) →
    ∀ (m : σ →₀ ℕ) (r : MvPolynomial σ R) (hmn : m ≤ n) (hrq : r ∣ q)
      (hp : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r), p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r

Tactic:
refine ⟨fun hp ↦ ?_, fun ⟨m, r, hmn, hrq, hp⟩ ↦ ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
rw : n ≠ 0
⊢ n.support.Nonempty

Tactic:
rw [Finsupp.support_nonempty_iff]

Premises used: Finsupp.support_nonempty_iff
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
hn' : n = 0
⊢ False

Tactic:
simp [hn'] at hn