awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
ab : A × A
hab : ab.1 ∈ f.support ∧ ab.2 ∈ g.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.2 = (a0, b0).2

Tactic:
(h hab.1 hab.2 he).2

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
ab : A × A
hab : ab.1 ∈ f.support ∧ ab.2 ∈ g.support
hne : ab ≠ (a0, b0)
he : ab.1 * ab.2 = a0 * b0
⊢ ab.1 = (a0, b0).1

Tactic:
exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]

Premises used: And.right, And.left
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
⊢ ¬(a0 ∈ f.support ∧ b0 ∈ g.support) →
    (if True then HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) else 0) = 0

Tactic:
fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)

Premises used: Iff.mpr, ite_eq_right_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
refine_2 :
  ∀ (hnotMem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)),
    True → HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0
⊢ ¬(a0 ∈ f.support ∧ b0 ∈ g.support) →
    (if True then HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) else 0) = 0

Tactic:
refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)

Premises used: Iff.mpr, ite_eq_right_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnotMem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
h_1 : True
refine_2 :
  ∀ (af : a0 ∉ f.support), HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0
refine_2₁ :
  ∀ (bg : b0 ∉ g.support), HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0

Tactic:
rcases not_and_or.mp hnotMem with af | bg

Premises used: not_and_or, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnotMem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
h_1 : True
af : a0 ∉ f.support
refine_2 : HMul.hMul (α := R) (β := R) (0 : R) ((g : (a : A) → R) b0 : R) = 0
refine_2₁ refine_2₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0

Tactic:
rw [notMem_support_iff.mp af, zero_mul]

Premises used: Finsupp.notMem_support_iff, MulZeroClass.zero_mul, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
hnotMem : ¬(a0 ∈ f.support ∧ b0 ∈ g.support)
h_1 : True
bg : b0 ∉ g.support
refine_2 : HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) (0 : R) = 0
refine_2₁ refine_2₂ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0

Tactic:
rw [notMem_support_iff.mp bg, mul_zero]

Premises used: Finsupp.notMem_support_iff, MulZeroClass.mul_zero, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.support g.support a0 b0
simp_rw :
  (sum f fun (m₁ : A) (r₁ : R) ↦ sum g fun (m₂ : A) (r₂ : R) ↦ if m₁ * m₂ = a0 * b0 then r₁ * r₂ else 0) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
simp_rw₁ :
  (∑ x ∈ f.support,
      ∑ x_1 ∈ g.support,
        if x * x_1 = a0 * b0 then HMul.hMul (α := R) (β := R) ((f : (a : A) → R) x : R) ((g : (a : A) → R) x_1 : R)
        else 0) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
simp_rw₂ :
  (∑ x ∈ f.support ×ˢ g.support,
      if x.1 * x.2 = a0 * b0 then HMul.hMul (α := R) (β := R) ((f : (a : A) → R) x.1 : R) ((g : (a : A) → R) x.2 : R)
      else 0) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
refine_1 :
  ∀ (b : A × A),
    b.1 ∈ f.support ∧ b.2 ∈ g.support →
      b ≠ (a0, b0) →
        (if b.1 * b.2 = a0 * b0 then HMul.hMul (α := R) (β := R) ((f : (a : A) → R) b.1 : R) ((g : (a : A) → R) b.2 : R)
          else 0) =
          0
refine_2 refine_2₁ :
  ¬(a0 ∈ f.support ∧ b0 ∈ g.support) →
    (if True then HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) else 0) = 0
⊢ (f * g : (a : A) → R) (a0 * b0) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)

Tactic:
classical
  simp_rw [mul_apply, sum, ← Finset.sum_product']
  refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl) <;> simp_rw [Finset.mem_product]
  · refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
    exacts [(h hab.1 hab.2 he).1, (h hab.1 hab.2 he).2]
  · refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)
    rcases not_and_or.mp hnotMem with af | bg
    · rw [notMem_support_iff.mp af, zero_mul]
    · rw [notMem_support_iff.mp bg, mul_zero]

Premises used: Iff.mpr, MulZeroClass.zero_mul, Finsupp.sum, Prod.mk, if_pos, Finset.sum_eq_single, Finset.sum_product', MulZeroClass.mul_zero, ite_eq_right_iff, MonoidAlgebra.mul_apply, Finset.mem_product, if_neg, rfl, Eq.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Mul A
inst_3 : UniqueProds A
a b : R[A]
ab : a * b = 0
contrapose! : ∀ (ab : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! ab
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Mul A
inst_3 : UniqueProds A
a b : R[A]
ab : a ≠ 0 ∧ b ≠ 0
obtain :
  ∀ (da : A) (a0 : da ∈ a.support) (db : A) (b0 : db ∈ b.support) (h : UniqueMul a.support b.support da db), a * b ≠ 0
⊢ a * b ≠ 0

Tactic:
obtain ⟨da, a0, db, b0, h⟩ := UniqueProds.uniqueMul_of_nonempty
      (support_nonempty_iff.mpr ab.1) (support_nonempty_iff.mpr ab.2)

Premises used: Iff.mpr, UniqueProds.uniqueMul_of_nonempty, Finsupp.support_nonempty_iff, And.right, And.left
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Mul A
inst_3 : UniqueProds A
a b : R[A]
ab : a ≠ 0 ∧ b ≠ 0
da : A
a0 : da ∈ a.support
db : A
b0 : db ∈ b.support
h : UniqueMul a.support b.support da db
⊢ a * b ≠ 0

Tactic:
support_nonempty_iff.mp ⟨da * db, ?_⟩

Premises used: HMul.hMul, Finsupp.support_nonempty_iff, MonoidAlgebra, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Mul A
inst_3 : UniqueProds A
a b : R[A]
ab : a ≠ 0 ∧ b ≠ 0
da : A
a0 : da ∈ a.support
db : A
b0 : db ∈ b.support
h : UniqueMul a.support b.support da db
refine : da * db ∈ (a * b).support
⊢ a * b ≠ 0

Tactic:
refine support_nonempty_iff.mp ⟨da * db, ?_⟩

Premises used: HMul.hMul, Finsupp.support_nonempty_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Mul A
inst_3 : UniqueProds A
a b : R[A]
ab : a ≠ 0 ∧ b ≠ 0
da : A
a0 : da ∈ a.support
db : A
b0 : db ∈ b.support
h : UniqueMul a.support b.support da db
rw :
  ∀ (a0 : Ne.{u_1 + 1} (α := R) ((a : (a : A) → R) da : R) (0 : R)) (db : A)
    (b0 : Ne.{u_1 + 1} (α := R) ((b : (a : A) → R) db : R) (0 : R)) (h : UniqueMul a.support b.support da db),
    Ne.{u_1 + 1} (α := R) ((a * b : (a : A) → R) (da * db) : R) (0 : R)
⊢ da * db ∈ (a * b).support

Tactic:
rw [mem_support_iff] at a0 b0 ⊢

Premises used: Finsupp.mem_support_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Mul A
inst_3 : UniqueProds A
a b : R[A]
ab : a ≠ 0 ∧ b ≠ 0
da : A
a0 : Ne.{u_1 + 1} (α := R) ((a : (a : A) → R) da : R) (0 : R)
db : A
b0 : Ne.{u_1 + 1} (α := R) ((b : (a : A) → R) db : R) (0 : R)
h : UniqueMul a.support b.support da db
⊢ Ne.{u_1 + 1} (α := R) ((a * b : (a : A) → R) (da * db) : R) (0 : R)

Tactic:
mul_apply_mul_eq_mul_of_uniqueMul h ▸ mul_ne_zero a0 b0

Premises used: Eq.rec, MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul, mul_ne_zero, Eq.symm
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : NoZeroDivisors R
inst_2 : Mul A
inst_3 : UniqueProds A
a b : R[A]
ab : a ≠ 0 ∧ b ≠ 0
da : A
a0 : Ne.{u_1 + 1} (α := R) ((a : (a : A) → R) da : R) (0 : R)
db : A
b0 : Ne.{u_1 + 1} (α := R) ((b : (a : A) → R) db : R) (0 : R)
h : UniqueMul a.support b.support da db
⊢ Ne.{u_1 + 1} (α := R) ((a * b : (a : A) → R) (da * db) : R) (0 : R)

Tactic:
exact mul_apply_mul_eq_mul_of_uniqueMul h ▸ mul_ne_zero a0 b0
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂))
      (hg : g₁.support ∪ g₂.support = s.erase s_1), g₁ = g₂
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
hg : g₁.support ∪ g₂.support = s
H : ∀ (h : s = ∅), g₁ = g₂
H₁ : ∀ (h : s.Nonempty), g₁ = g₂
⊢ g₁ = g₂

Tactic:
obtain h | h := s.eq_empty_or_nonempty

Premises used: Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂))
      (hg : g₁.support ∪ g₂.support = s.erase s_1), g₁ = g₂
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
hg : g₁.support ∪ g₂.support = s
h : s = ∅
⊢ ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1

Tactic:
subst s
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂))
      (hg : g₁.support ∪ g₂.support = s.erase s_1), g₁ = g₂
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
hg : g₁.support ∪ g₂.support = s
h : s = ∅
ih₁ :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
⊢ g₁.support ∪ g₂.support = ∅

Tactic:
subst s
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂))
      (hg : g₁.support ∪ g₂.support = s.erase s_1), g₁ = g₂
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
hg : g₁.support ∪ g₂.support = s
h : s.Nonempty
⊢ ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1

Tactic:
subst s
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
s : Finset A
ih :
  ∀ s_1 ∈ s,
    ∀ {g₁ g₂ : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂))
      (hg : g₁.support ∪ g₂.support = s.erase s_1), g₁ = g₂
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
hg : g₁.support ∪ g₂.support = s
h : s.Nonempty
ih₁ :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
⊢ (g₁.support ∪ g₂.support).Nonempty

Tactic:
subst s
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h : g₁.support ∪ g₂.support = ∅
⊢ g₁ = 0 ∧ g₂ = 0

Tactic:
simp_rw [Finset.union_eq_empty, support_eq_empty] at h

Premises used: Finset.union_eq_empty, Finsupp.support_eq_empty
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h : g₁ = 0 ∧ g₂ = 0
⊢ g₁ = g₂

Tactic:
h.1.trans h.2.symm

Premises used: And.right, And.left, MonoidAlgebra, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h : g₁ = 0 ∧ g₂ = 0
⊢ g₁ = g₂

Tactic:
exact h.1.trans h.2.symm

Premises used: And.right, And.left, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h : (g₁.support ∪ g₂.support).Nonempty
H :
  ∀ (af : A) (haf : af ∈ f.support) (ag : A) (hag : ag ∈ g₁.support ∪ g₂.support)
    (uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag), g₁ = g₂
⊢ g₁ = g₂

Tactic:
obtain ⟨af, haf, ag, hag, uniq⟩ :=
      UniqueProds.uniqueMul_of_nonempty (support_nonempty_iff.2 hf) h

Premises used: Iff.mpr, UniqueProds.uniqueMul_of_nonempty, Finsupp.support_nonempty_iff
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁) ((fun (x : R[A]) ↦ f * x) g₂)
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h : (g₁.support ∪ g₂.support).Nonempty
af : A
haf : af ∈ f.support
ag : A
hag : ag ∈ g₁.support ∪ g₂.support
uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag
⊢ (f * g₁ : (a : A) → R) (af * ag) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)

Tactic:
have h := mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : f * g₁ = f * g₂
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h_1 : (g₁.support ∪ g₂.support).Nonempty
af : A
haf : af ∈ f.support
ag : A
hag : ag ∈ g₁.support ∪ g₂.support
uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag
h :
  (f * g₁ : (a : A) → R) (af * ag) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₂ : (a : A) → R) ag : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)

Tactic:
rw [eq, mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h

Premises used: UniqueMul.mono, MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul, Finset.subset_union_right, subset_rfl
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : f * g₁ = f * g₂
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h_1 : (g₁.support ∪ g₂.support).Nonempty
af : A
haf : af ∈ f.support
ag : A
hag : ag ∈ g₁.support ∪ g₂.support
uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag
h :
  HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₂ : (a : A) → R) ag : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)
⊢ Eq.{u_1 + 1} (α := R) ((g₂ : (a : A) → R) ag : R) ((g₁ : (a : A) → R) ag : R)

Tactic:
have := mul_left_cancel₀ (mem_support_iff.mp haf) h
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : f * g₁ = f * g₂
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h_1 : (g₁.support ∪ g₂.support).Nonempty
af : A
haf : af ∈ f.support
ag : A
hag : ag ∈ g₁.support ∪ g₂.support
uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag
h :
  HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₂ : (a : A) → R) ag : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)
this : Eq.{u_1 + 1} (α := R) ((g₂ : (a : A) → R) ag : R) ((g₁ : (a : A) → R) ag : R)
H :
  ∀
    (eq :
      f * HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₁) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R) =
        f * HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₂) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R))
    (hag : ag ∈ g₁.support ∪ g₂.support) (uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag)
    (h :
      HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₂ : (a : A) → R) ag : R) =
        HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R))
    (this : Eq.{u_1 + 1} (α := R) ((g₂ : (a : A) → R) ag : R) ((g₁ : (a : A) → R) ag : R)),
    HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₁) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R) =
      HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₂) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R)
⊢ g₁ = g₂

Tactic:
rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢

Premises used: Finsupp.erase_add_single
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h_1 : (g₁.support ∪ g₂.support).Nonempty
af : A
haf : af ∈ f.support
ag : A
eq :
  f * HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₁) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R) =
    f * HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₂) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R)
hag : ag ∈ g₁.support ∪ g₂.support
uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag
h :
  HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₂ : (a : A) → R) ag : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)
this : Eq.{u_1 + 1} (α := R) ((g₂ : (a : A) → R) ag : R) ((g₁ : (a : A) → R) ag : R)
⊢ f * Finsupp.erase ag g₁ = f * Finsupp.erase ag g₂

Tactic:
simp_rw [mul_add, add_right_cancel_iff] at eq

Premises used: add_right_cancel_iff, mul_add
-- Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
Goal:
R : Type u_1
A : Type u_2
inst : Semiring R
inst_1 : IsCancelAdd R
inst_2 : IsLeftCancelMulZero R
inst_3 : Mul A
inst_4 : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.support ∪ g₂.support,
    ∀ {g₁_1 g₂_1 : R[A]} (eq : Eq (α := R[A]) ((fun (x : R[A]) ↦ f * x) g₁_1) ((fun (x : R[A]) ↦ f * x) g₂_1))
      (hg : g₁_1.support ∪ g₂_1.support = (g₁.support ∪ g₂.support).erase s), g₁_1 = g₂_1
h_1 : (g₁.support ∪ g₂.support).Nonempty
af : A
haf : af ∈ f.support
ag : A
hag : ag ∈ g₁.support ∪ g₂.support
uniq : UniqueMul f.support (g₁.support ∪ g₂.support) af ag
h :
  HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₂ : (a : A) → R) ag : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : A) → R) af : R) ((g₁ : (a : A) → R) ag : R)
this : Eq.{u_1 + 1} (α := R) ((g₂ : (a : A) → R) ag : R) ((g₁ : (a : A) → R) ag : R)
eq : f * Finsupp.erase ag g₁ = f * Finsupp.erase ag g₂
H : (Finsupp.erase ag g₁).support ∪ (Finsupp.erase ag g₂).support = (g₁.support ∪ g₂.support).erase ag
⊢ HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₁) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R) =
    HAdd.hAdd (β := A →₀ R) (Finsupp.erase ag g₂) (Finsupp.single ag ((g₁ : (a : A) → R) ag) : A →₀ R)

Tactic:
rw [ih ag hag eq]