awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Nontrivial R
i j : σ
simp_rw : LE.le (α := ℕ) (1 : ℕ) ((Finsupp.single j 1 : (a : σ) → ℕ) i : ℕ) ↔ i = j
simp_rw₁ : Ne (α := ℕ) ((Finsupp.single j 1 : (a : σ) → ℕ) i : ℕ) (0 : ℕ) ↔ i = j
simp_rw₂ : i = j ∧ Ne (α := ℕ) 1 0 ↔ i = j
simp_rw₃ : i = j ∧ ¬Eq (α := ℕ) 1 0 ↔ i = j
simp_rw₄ : i = j ∧ ¬False ↔ i = j
⊢ LE.le (α := σ →₀ ℕ) (Finsupp.single i 1) (Finsupp.single j 1) ↔ i = j
have simp_rw₅ : i = j ∧ True ↔ i = j
Tactic: simp_rw [Finsupp.single_le_iff, Nat.one_le_iff_ne_zero, Finsupp.single_apply_ne_zero,
    ne_eq, reduceCtorEq, not_false_eq_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ Dvd.dvd (α := MvPolynomial σ R) (X i) ((monomial j : (a : R) → MvPolynomial σ R) r) ↔
    r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have refine : (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: refine monomial_dvd_monomial.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have simp_rw : (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ True ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
simp_rw : (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ True ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have simp_rw₁ : r = 0 ∨ Finsupp.single i 1 ≤ j ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
simp_rw : (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ True ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
simp_rw₁ : r = 0 ∨ Finsupp.single i 1 ≤ j ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ 1 ∣ r ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have simp_rw₂ : r = 0 ∨ LE.le (α := ℕ) (1 : ℕ) ((j : (a : σ) → ℕ) i : ℕ) ↔ r = 0 ∨ Ne (α := ℕ) ((j : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: simp_rw [one_dvd, and_true, Finsupp.single_le_iff, Nat.one_le_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ q = p.divMonomial (Finsupp.single i 1)
have a : ∀ (n : σ →₀ ℕ), coeff n q = coeff n (p.divMonomial (Finsupp.single i 1))
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
n : σ →₀ ℕ
⊢ coeff n q = coeff n (p.divMonomial (Finsupp.single i 1))
have a : Finsupp.single i 1 + n ∉ r.support
Tactic: rw [coeff_divMonomial, h, coeff_add, coeff_X_mul, left_eq_add, ← notMem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
⊢ IsCancelAdd (MvPolynomial σ R)
have suffices : IsLeftCancelAdd (MvPolynomial σ R)
Tactic: suffices IsLeftCancelAdd (MvPolynomial σ R) from
    AddCommMagma.IsLeftCancelAdd.toIsCancelAdd _
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : IsLeftCancelAdd R
⊢ IsLeftCancelAdd (MvPolynomial σ R)
have 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
Tactic: refine { add_left_cancel := fun f g h H ↦ ?_ }
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ g = h
have a : ∀ (d : σ →₀ ℕ), coeff d g = coeff d h
Tactic: ext d
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ r = p.modMonomial (Finsupp.single i 1)
have 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)
Tactic: rwa [← p.divMonomial_add_modMonomial_single i,
    eq_divMonomial_single h hr, add_right_inj, eq_comm] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ r = p.modMonomial (Finsupp.single i 1)
have 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)
Tactic: rwa [← p.divMonomial_add_modMonomial_single i,
    eq_divMonomial_single h hr, add_right_inj, eq_comm] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ r = p.modMonomial (Finsupp.single i 1)
have rwa₂ : ∀ (h' : p.modMonomial (Finsupp.single i 1) = r), 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'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ r = p.modMonomial (Finsupp.single i 1)
have rwa₃ : ∀ (h' : 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'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
have refine_1 : ∀ (h : r = p.modMonomial (Finsupp.single i 1)), ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: refine ⟨fun h n ↦ ?_, fun hr ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ r = p.modMonomial (Finsupp.single i 1) ↔ ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have refine_2 : ∀ (hr : ∀ n ∈ r.support, Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)), r = p.modMonomial (Finsupp.single i 1)
Tactic: refine ⟨fun h n ↦ ?_, fun hr ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : σ →₀ ℕ
⊢ n ∈ r.support → Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have refine_1 : Ne (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ) → n ∉ r.support
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ n ∉ r.support
have refine_1 : coeff n (p.modMonomial (Finsupp.single i 1)) = 0
Tactic: rw [h, notMem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ coeff n (p.modMonomial (Finsupp.single i 1)) = 0
have refine_1 : Finsupp.single i 1 ≤ n
Tactic: apply coeff_modMonomial_of_le
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ r = p.modMonomial (Finsupp.single i 1)
have refine_2 : ∀ (q : MvPolynomial σ R) (hq : p - r = X i * q), r = p.modMonomial (Finsupp.single i 1)
Tactic: obtain ⟨q, hq⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ r = p.modMonomial (Finsupp.single i 1)
have apply : p = X i * q + r
Tactic: apply eq_modMonomial_single (q := q) _ hr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
⊢ X i ∣ p * q ↔ X i ∣ p ∨ X i ∣ q
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
i : σ
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
h : Nontrivial R
⊢ X i ∣ p * q ↔ X i ∣ p ∨ X i ∣ q
have x : NoZeroDivisors (MvPolynomial σ R)
Tactic: have _ : NoZeroDivisors (MvPolynomial σ R) :=
    IsLeftCancelMulZero.to_noZeroDivisors (MvPolynomial σ R)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ X i ∣ p * q ↔ X i ∣ p ∨ X i ∣ q
have mp : X i ∣ p * q → X i ∣ p ∨ X i ∣ q
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ X i ∣ p * q ↔ X i ∣ p ∨ X i ∣ q
have mpr : X i ∣ p ∨ X i ∣ q → X i ∣ p * q
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
⊢ X i ∣ p ∨ X i ∣ q
have simp : ∀ (h : (p * q).modMonomial (Finsupp.single i 1) = 0),
  p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0
Tactic: simp only [X_dvd_iff_modMonomial_eq_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0
have 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
Tactic: rwa [h, mul_eq_zero] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ p.modMonomial (Finsupp.single i 1) = 0 ∨ q.modMonomial (Finsupp.single i 1) = 0
have 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
Tactic: rwa [h, mul_eq_zero] at this
Cleared hypotheses: this, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ X i ∣ p ∨ X i ∣ q
have mp : p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
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
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
have hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
Tactic: have hq := q.modMonomial_add_divMonomial_single i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
have mp : ∀ n ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support,
  Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: rw [eq_modMonomial_single_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1) = (p * q).modMonomial (Finsupp.single i 1)
have mp₁ : X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
Tactic: rw [eq_modMonomial_single_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : σ →₀ ℕ
⊢ n ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support →
    Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
have mp : ¬Eq (α := ℕ) ((n : (a : σ) → ℕ) i : ℕ) (0 : ℕ) →
  n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
have 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
Tactic: rw [notMem_support_iff, coeff_mul]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ 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
have 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
Tactic: apply Finset.sum_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
have hx₁ : x.1 + x.2 = n
Tactic: simp only [Finset.mem_antidiagonal] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
have hn₁ : ¬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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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 : ℕ)
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
have 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
Tactic: rcases hn with hn | hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
have 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
Tactic: rcases hn with hn | hn
Cleared hypotheses: hn