awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
suffices : IsLeftCancelAdd (MvPolynomial σ R)
⊢ IsCancelAdd (MvPolynomial σ R)

Tactic:
suffices IsLeftCancelAdd (MvPolynomial σ R) from
    AddCommMagma.IsLeftCancelAdd.toIsCancelAdd _
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
⊢ IsLeftCancelAdd (MvPolynomial σ R)

Tactic:
{ add_left_cancel := fun f g h H ↦ ?_ }

Premises used: IsLeftCancelAdd.mk
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
refine :
  ∀ (f g h : MvPolynomial σ R)
    (H : Eq (α := MvPolynomial σ R) ((fun (x : MvPolynomial σ R) ↦ f + x) g) ((fun (x : MvPolynomial σ R) ↦ f + x) h)),
    g = h
⊢ IsLeftCancelAdd (MvPolynomial σ R)

Tactic:
refine { add_left_cancel := fun f g h H ↦ ?_ }
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
f g h : MvPolynomial σ R
H : Eq (α := MvPolynomial σ R) ((fun (x : MvPolynomial σ R) ↦ f + x) g) ((fun (x : MvPolynomial σ R) ↦ f + x) h)
a : ∀ (d : σ →₀ ℕ), coeff d g = coeff d h
⊢ g = h

Tactic:
ext d
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
f g h : MvPolynomial σ R
H : Eq (α := MvPolynomial σ R) ((fun (x : MvPolynomial σ R) ↦ f + x) g) ((fun (x : MvPolynomial σ R) ↦ f + x) h)
d : σ →₀ ℕ
⊢ coeff d g = coeff d h

Tactic:
simpa using congr_arg (coeff d) H

Premises used: MvPolynomial.coeff, congr_arg
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
σ : Type u_3
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ p = X i * q + r

Tactic:
have h' := id h
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
σ : Type u_3
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
h' : p = X i * q + r
rwa :
  ∀ (h' : X i * p.divMonomial (Finsupp.single i 1) + p.modMonomial (Finsupp.single i 1) = X i * q + r),
    r = p.modMonomial (Finsupp.single i 1)
rwa₁ :
  ∀
    (h' :
      X i * p.divMonomial (Finsupp.single i 1) + p.modMonomial (Finsupp.single i 1) =
        X i * p.divMonomial (Finsupp.single i 1) + r),
    r = p.modMonomial (Finsupp.single i 1)
rwa₂ : ∀ (h' : p.modMonomial (Finsupp.single i 1) = r), r = p.modMonomial (Finsupp.single i 1)
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h' : r = p.modMonomial (Finsupp.single i 1)), r = p.modMonomial (Finsupp.single i 1)
⊢ r = p.modMonomial (Finsupp.single i 1)

Tactic:
rwa [← p.divMonomial_add_modMonomial_single i,
    eq_divMonomial_single h hr, add_right_inj, eq_comm] at h'

Premises used: MvPolynomial.eq_divMonomial_single, eq_comm, MvPolynomial.divMonomial_add_modMonomial_single, add_right_inj
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
h : X i ∣ p - r
⊢ r = p.modMonomial (Finsupp.single i 1) ↔ ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
⟨fun h n ↦ ?_, fun hr ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
h : X i ∣ p - r
refine_1 :
  ∀ (h : r = p.modMonomial (Finsupp.single i 1)), ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
refine_2 :
  ∀ (hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), r = p.modMonomial (Finsupp.single i 1)
⊢ r = p.modMonomial (Finsupp.single i 1) ↔ ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
refine ⟨fun h n ↦ ?_, fun hr ↦ ?_⟩
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
h_1 : X i ∣ p - r
h : r = p.modMonomial (Finsupp.single i 1)
n : σ →₀ ℕ
refine_1 : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → n ∉ r.support
⊢ n ∈ r.support → Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
contrapose!
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
h_1 : X i ∣ p - r
h : r = p.modMonomial (Finsupp.single i 1)
n : σ →₀ ℕ
hn : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
refine_1 : coeff n (p.modMonomial (Finsupp.single i 1)) = 0
⊢ n ∉ r.support

Tactic:
rw [h, notMem_support_iff]

Premises used: MvPolynomial.notMem_support_iff
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
h_1 : X i ∣ p - r
h : r = p.modMonomial (Finsupp.single i 1)
n : σ →₀ ℕ
hn : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
refine_1 : Finsupp.single i 1 ≤ n
⊢ coeff n (p.modMonomial (Finsupp.single i 1)) = 0

Tactic:
apply coeff_modMonomial_of_le

Premises used: MvPolynomial.coeff_modMonomial_of_le
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
h_1 : X i ∣ p - r
h : r = p.modMonomial (Finsupp.single i 1)
n : σ →₀ ℕ
hn : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Finsupp.single i 1 ≤ n

Tactic:
simpa [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
h : X i ∣ p - r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
refine_2 : ∀ (q : MvPolynomial σ R) (hq : p - r = X i * q), r = p.modMonomial (Finsupp.single i 1)
⊢ r = p.modMonomial (Finsupp.single i 1)

Tactic:
obtain ⟨q, hq⟩ := h
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
q : MvPolynomial σ R
hq : p - r = X i * q
apply : p = X i * q + r
⊢ r = p.modMonomial (Finsupp.single i 1)

Tactic:
apply eq_modMonomial_single (q := q) _ hr

Premises used: MvPolynomial.eq_modMonomial_single
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p r : MvPolynomial σ R
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
q : MvPolynomial σ R
hq : p - r = X i * q
rwa rwa₁ rwa₂ rwa₃ : p - r = X i * q
⊢ p = X i * q + r

Tactic:
rwa [← sub_eq_iff_eq_add]

Premises used: sub_eq_iff_eq_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
⊢ Nontrivial R

Tactic:
nontriviality 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
h : Nontrivial R
⊢ NoZeroDivisors (MvPolynomial σ R)

Tactic:
have _ : NoZeroDivisors (MvPolynomial σ R) :=
    IsLeftCancelMulZero.to_noZeroDivisors (MvPolynomial σ 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
h : Nontrivial R
h_1 : NoZeroDivisors (MvPolynomial σ R)
mp : X i ∣ p * q → X i ∣ p ∨ X i ∣ q
mpr : X i ∣ p ∨ X i ∣ q → X i ∣ p * q
⊢ X i ∣ p * q ↔ X i ∣ p ∨ X i ∣ 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
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ p * q
this :
  p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
simp :
  ∀ (h : (p * q).modMonomial (Finsupp.single i 1) = 0),
    p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0
⊢ X i ∣ p ∨ X i ∣ q

Tactic:
simp only [X_dvd_iff_modMonomial_eq_zero] at h ⊢

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
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
this :
  p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
h : (p * q).modMonomial (Finsupp.single i 1) = 0
rwa :
  ∀ (this : p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = 0)
    (h : (p * q).modMonomial (Finsupp.single i 1) = 0),
    p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0)
    (h : (p * q).modMonomial (Finsupp.single i 1) = 0),
    p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0
⊢ p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0

Tactic:
rwa [h, mul_eq_zero] at this

Premises used: mul_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
h_1 : Nontrivial R
h_2 : NoZeroDivisors (MvPolynomial σ R)
h : X i ∣ p * q
mp : p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
⊢ X i ∣ p ∨ X i ∣ q

Tactic:
suffices (p.modMonomial (Finsupp.single i 1)) * (q.modMonomial (Finsupp.single i 1)) =
          (p * q).modMonomial (Finsupp.single i 1) by
      simp only [X_dvd_iff_modMonomial_eq_zero] at h ⊢
      rwa [h, mul_eq_zero] at 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
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
⊢ q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q

Tactic:
have hq := q.modMonomial_add_divMonomial_single i
-- 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 :
  ∀ n ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support,
    Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
mp₁ : X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
⊢ p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)

Tactic:
rw [eq_modMonomial_single_iff]

Premises used: MvPolynomial.eq_modMonomial_single_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
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
n : σ →₀ ℕ
mp :
  ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ) →
    n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
⊢ n ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support →
    Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
contrapose
-- 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
n : σ →₀ ℕ
hn : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
mp :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
      coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)))
    0
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support

Tactic:
rw [notMem_support_iff, coeff_mul]

Premises used: MvPolynomial.notMem_support_iff, MvPolynomial.coeff_mul
-- 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
n : σ →₀ ℕ
hn : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
mp :
  ∀ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
⊢ Eq.{u_3 + 1} (α := R)
    (∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
      coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)))
    0

Tactic:
apply Finset.sum_eq_zero

Premises used: Finset.sum_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
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
n : σ →₀ ℕ
hn : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n
⊢ x.1 + x.2 = n

Tactic:
simp only [Finset.mem_antidiagonal] at hx

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- 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
n : σ →₀ ℕ
hn : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
⊢ ¬Eq (α := ℕ) ((x.1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ) ∨ ¬Eq (α := ℕ) ((x.2 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simp only [← hx, Finsupp.coe_add, Pi.add_apply, Nat.add_eq_zero_iff, not_and_or] at hn

Premises used: Pi.add_apply, Finsupp.coe_add, not_and_or, Nat.add_eq_zero_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
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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
hn : ¬Eq (α := ℕ) ((x.1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ) ∨ ¬Eq (α := ℕ) ((x.2 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
mp :
  ∀ (hn : ¬Eq (α := ℕ) ((x.1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
mp₁ :
  ∀ (hn : ¬Eq (α := ℕ) ((x.2 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0

Tactic:
rcases hn with hn | hn
-- 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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
hn : ¬Eq (α := ℕ) ((x.1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
mp : Finsupp.single i 1 ≤ x.1
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0

Tactic:
rw [coeff_modMonomial_of_le, zero_mul]

Premises used: MulZeroClass.zero_mul, MvPolynomial.coeff_modMonomial_of_le
-- 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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
hn : ¬Eq (α := ℕ) ((x.1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Finsupp.single i 1 ≤ x.1

Tactic:
simpa [← Nat.one_le_iff_ne_zero] using hn

Premises used: Nat.one_le_iff_ne_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
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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
hn : ¬Eq (α := ℕ) ((x.2 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
mp : Finsupp.single i 1 ≤ x.2
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0

Tactic:
rw [mul_comm, coeff_modMonomial_of_le, zero_mul]

Premises used: MulZeroClass.zero_mul, MvPolynomial.coeff_modMonomial_of_le, 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
n : σ →₀ ℕ
x : (σ →₀ ℕ) × (σ →₀ ℕ)
hx : x.1 + x.2 = n
hn : ¬Eq (α := ℕ) ((x.2 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ Finsupp.single i 1 ≤ x.2

Tactic:
simpa [← Nat.one_le_iff_ne_zero] using hn

Premises used: Nat.one_le_iff_ne_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
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
n : σ →₀ ℕ
hn : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
mp : coeff n (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)) = 0
mp₁ mp₂ mp₃ :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n,
      coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)))
    0
mp₄ mp₅ :
  ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x ∈ @Finset.antidiagonal _ Finsupp.instAddMonoid _ n),
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
mp₆ :
  ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = n),
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
mp₇ :
  ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = n)
    (hn : ¬Eq (α := ℕ) ((x.1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ) ∨ ¬Eq (α := ℕ) ((x.2 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
mp₈ :
  ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = n) (hn : ¬Eq (α := ℕ) ((x.1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
mp₉ mp₁₀ :
  ∀ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) (hx : x.1 + x.2 = n) (hn : ¬Eq (α := ℕ) ((x.2 : (a : σ) → ℕ) i : ℕ) (0 : ℕ)),
    coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support

Tactic:
classical
      rw [notMem_support_iff, coeff_mul]
      apply Finset.sum_eq_zero
      intro x hx
      simp only [Finset.mem_antidiagonal] at hx
      simp only [← hx, Finsupp.coe_add, Pi.add_apply, Nat.add_eq_zero_iff, not_and_or] at hn
      rcases hn with hn | hn
      · rw [coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn
      · rw [mul_comm, coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn

Premises used: MvPolynomial.notMem_support_iff, MulZeroClass.zero_mul, Finset.sum_eq_zero, MvPolynomial.coeff_modMonomial_of_le, Pi.add_apply, Finsupp.coe_add, Finset.HasAntidiagonal.mem_antidiagonal, not_and_or, mul_comm, Nat.one_le_iff_ne_zero, Nat.add_eq_zero_iff, MvPolynomial.coeff_mul
-- 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 ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) * q -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
nth_rewrite 1 [← 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
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 ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) *
        (q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1)) -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
⊢ X i ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) * q -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
nth_rewrite 1 [← 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
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) * (X i * q.divMonomial (Finsupp.single i 1)) +
        X i * p.divMonomial (Finsupp.single i 1) * (X i * q.divMonomial (Finsupp.single i 1)))
⊢ X i ∣
    (p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1)) *
        (q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1)) -
      p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
simp only [add_mul, mul_add, add_assoc, add_sub_cancel_left]

Premises used: add_mul, add_sub_cancel_left, add_assoc, mul_add