awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0
have refine_2₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [notMem_support_iff.mp bg, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ (f * g : (a : A) → R) (a0 * b0) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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)
⊢ (f * g : (a : A) → R) (a0 * b0) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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)
⊢ (f * g : (a : A) → R) (a0 * b0) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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)
⊢ (f * g : (a : A) → R) (a0 * b0) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ (f * g : (a : A) → R) (a0 * b0) = HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R)
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ a = 0 ∨ b = 0
have contrapose! : ∀ (ab : a ≠ 0 ∧ b ≠ 0), a * b ≠ 0
Tactic: contrapose! ab
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ a * b ≠ 0
have obtain : ∀ (da : A) (a0 : da ∈ a.support) (db : A) (b0 : db ∈ b.support) (h : UniqueMul a.support b.support da db), 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)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
have refine : da * db ∈ (a * b).support
Tactic: refine support_nonempty_iff.mp ⟨da * db, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ da * db ∈ (a * b).support
have 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)
Tactic: rw [mem_support_iff] at a0 b0 ⊢
Cleared hypotheses: a0, db, b0, h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ g₁ = g₂
have H : ∀ (h : s = ∅), g₁ = g₂
Tactic: obtain h | h := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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₂
⊢ g₁ = g₂
have H₁ : ∀ (h : s.Nonempty), g₁ = g₂
Tactic: obtain h | h := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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 = ∅
⊢ g₁ = g₂
have 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
Tactic: subst s
Cleared hypotheses: s, ih, hg, h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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₁ = g₂
have h₁ : g₁.support ∪ g₂.support = ∅
Tactic: subst s
Cleared hypotheses: s, ih, hg, h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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
⊢ g₁ = g₂
have 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
Tactic: subst s
Cleared hypotheses: s, ih, hg, h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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₁ = g₂
have h₁ : (g₁.support ∪ g₂.support).Nonempty
Tactic: subst s
Cleared hypotheses: s, ih, hg, h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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₁ = g₂
have h₁ : g₁ = 0 ∧ g₂ = 0
Tactic: simp_rw [Finset.union_eq_empty, support_eq_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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
⊢ g₁ = g₂
have 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₂
Tactic: obtain ⟨af, haf, ag, hag, uniq⟩ :=
      UniqueProds.uniqueMul_of_nonempty (support_nonempty_iff.2 hf) h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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
⊢ g₁ = g₂
have h₁ : (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)
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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)
⊢ g₁ = g₂
have 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)
Tactic: rw [eq, mul_apply_mul_eq_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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)
⊢ g₁ = g₂
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (goal)
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)
⊢ g₁ = g₂
have 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)
Tactic: rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
Cleared hypotheses: eq, hag, uniq, h, this
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors (hypothesis)
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)
⊢ 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)
have eq₁ : f * Finsupp.erase ag g₁ = f * Finsupp.erase ag g₂
Tactic: simp_rw [mul_add, add_right_cancel_iff] at eq
Cleared hypotheses: eq