awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ)
⊢ coeff x.1 (p.modMonomial (Finsupp.single i 1)) * coeff x.2 (q.modMonomial (Finsupp.single i 1)) = 0
have mp : Finsupp.single i 1 ≤ x.1
Tactic: rw [coeff_modMonomial_of_le, zero_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 : σ →₀ ℕ
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
have mp : Finsupp.single i 1 ≤ x.2
Tactic: rw [mul_comm, coeff_modMonomial_of_le, zero_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 : ℕ)
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
have mp : coeff n (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)) = 0
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
-- 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 : ℕ)
mp : coeff n (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)) = 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: 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
-- 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 : ℕ)
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
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
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: 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
-- 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 : ℕ)
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
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
have 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
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
-- 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 : ℕ)
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
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
have 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
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
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 : σ →₀ ℕ
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
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
have 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
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
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 : σ →₀ ℕ
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
⊢ n ∉ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support
have 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
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
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
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
have 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)
Tactic: nth_rewrite 1 [← hp]
-- 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
⊢ 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)
have 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)
Tactic: nth_rewrite 1 [← hq]
-- 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
⊢ 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)
have 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)))
Tactic: simp only [add_mul, mul_add, add_assoc, add_sub_cancel_left]
-- 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
⊢ 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)))
have 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))
Tactic: simp only [← mul_assoc, mul_comm _ (X 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
⊢ 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))
have 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))))
Tactic: simp only [mul_assoc, ← mul_add (X i)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
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)
have refine : ¬IsUnit (M := MvPolynomial σ R) (X i)
Tactic: refine ⟨X_ne_zero i, ?_, fun p q ↦ X_dvd_mul_iff.mp⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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)
⊢ False
have h₁ : ∃ (b : MvPolynomial σ R), X i * b = 1 ∧ b * X i = 1
Tactic: rw [isUnit_iff_exists] 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 : σ
inst_1 : IsCancelMulZero R
inst_2 : Nontrivial R
h : ∃ (b : MvPolynomial σ R), X i * b = 1 ∧ b * X i = 1
⊢ False
have rcases : ∀ (u : MvPolynomial σ R) (hu : X i * u = 1), False
Tactic: rcases h with ⟨u, hu, -⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (hypothesis)
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
⊢ False
have hu₁ : 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
Cleared hypotheses: hu
-- 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
⊢ p ∣ X i * q ↔ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
have mp : p ∣ X i * q → p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ 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
mp : p ∣ X i * q → p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
⊢ p ∣ X i * q ↔ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
have mpr : p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q → p ∣ X i * q
Tactic: constructor
-- 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
r : MvPolynomial σ R
hp : X i * q = p * r
⊢ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
have this : X i ∣ p ∨ X i ∣ r
Tactic: have : X i ∣ p ∨ X i ∣ r := by simp [← X_dvd_mul_iff, ← hp]
-- 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
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
⊢ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
have mp : X i ∣ r → p ∣ q
Tactic: apply this.symm.imp
-- 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
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
mp : X i ∣ r → p ∣ q
⊢ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
have mp₁ : X i ∣ p → X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q
Tactic: apply this.symm.imp
-- 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
r : MvPolynomial σ R
hp : X i * q = p * (X i * r)
this : X i ∣ p ∨ X i ∣ X i * r
⊢ q = p * r
have rw : X i * q = X i * (p * r)
Tactic: rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]
-- 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
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)
⊢ q = p * r
have rw₁ : p * (X i * r) = X i * (p * r)
Tactic: rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]
-- 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
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)
⊢ q = p * r
have rw₂ : X i * (p * r) = X i * (p * r)
Tactic: rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]
-- 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
r : MvPolynomial σ R
hp : X i * q = p * (X i * r)
this : X i ∣ p ∨ X i ∣ X i * r
⊢ p ∣ q
have mp : ∀ (hp : X i * (p * r) = p * (X i * r)), p ∣ p * r
Tactic: obtain rfl : q = p * r := by rw [← X_mul_cancel_left_iff (i := i), hp, mul_left_comm]
Cleared hypotheses: q, hp
-- 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
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
have mp : p.divMonomial (Finsupp.single i 1) ∣ q
Tactic: refine ⟨hip, ?_⟩