awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddMonoid M
inst_2 : Nontrivial R
m : M
s : Set M
h :
  Membership.mem (γ := Submodule R R[M]) (Submodule.span R (↑(Submonoid.closure (of' R M '' s)) : Set R[M])) (of' R M m)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure s) m
have suffices : Membership.mem (α := Multiplicative M) (γ := Submonoid (Multiplicative M))
  (Submonoid.closure ((⇑Multiplicative.toAdd : (a : Multiplicative M) → M) ⁻¹' s))
  ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M)
Tactic: suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' s) by
    simpa [← AddSubmonoid.toSubmonoid_closure]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddMonoid M
inst_2 : Nontrivial R
m : M
s : Set M
h :
  Membership.mem (γ := Submodule R R[M]) (Submodule.span R (↑(Submonoid.closure (of' R M '' s)) : Set R[M])) (of' R M m)
s' : Submonoid (Multiplicative M) := Submonoid.closure s
⊢ Membership.mem (α := Multiplicative M) (γ := Submonoid (Multiplicative M))
    (Submonoid.closure ((⇑Multiplicative.toAdd : (a : Multiplicative M) → M) ⁻¹' s))
    ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M)
have h' : Eq (α := Submonoid R[M]) (Submonoid.map (F := Multiplicative M →* R[M]) (of R M) s')
  (Submonoid.closure ((⇑(of R M) : (a : Multiplicative M) → R[M]) '' s))
Tactic: have h' : Submonoid.map (of R M) s' = Submonoid.closure (of R M '' s) :=
    MonoidHom.map_mclosure _ _
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (hypothesis)
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddMonoid M
inst_2 : Nontrivial R
m : M
s : Set M
h :
  Membership.mem (γ := Submodule R R[M]) (Submodule.span R (↑(Submonoid.closure (of' R M '' s)) : Set R[M])) (of' R M m)
s' : Submonoid (Multiplicative M) := Submonoid.closure s
h' :
  Eq (α := Submonoid R[M]) (Submonoid.map (F := Multiplicative M →* R[M]) (of R M) s')
    (Submonoid.closure ((⇑(of R M) : (a : Multiplicative M) → R[M]) '' s))
⊢ Membership.mem (α := Multiplicative M) (γ := Submonoid (Multiplicative M))
    (Submonoid.closure ((⇑Multiplicative.toAdd : (a : Multiplicative M) → M) ⁻¹' s))
    ((Multiplicative.ofAdd : (a : M) → Multiplicative M) m : Multiplicative M)
have h₁ : let s' : Submonoid (Multiplicative M) := Submonoid.closure s;
Membership.mem (γ := Submodule R R[M])
  (Submodule.span R (↑(Submonoid.map (F := Multiplicative M →* R[M]) (of R M) s') : Set R[M])) (of' R M m)
Tactic: rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h
Cleared hypotheses: h, s', h'
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
⊢ (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (c • φ) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) φ : R)
have suffices : Eq (α := S[M] →+ R)
  (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
    ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
  (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
    (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
Tactic: suffices (liftNC (↑f) g).comp (smulAddHom S S[M] c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC f g) from DFunLike.congr_fun this φ
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
⊢ Eq (α := S[M] →+ R)
    (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
      ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
    (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
      (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
have hfg : ∀ (m : M) (x : S),
  Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
                (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
m : M
x : S
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
                (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg : Eq.{u_2 + 1} (α := R)
  ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
      ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
          ((singleAddHom m : (a : S) → S[M]) x) :
        S[M]) :
    R)
  (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
          ((singleAddHom m : (a : S) → S[M]) x : S[M]) :
        R) :
    R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
            ((singleAddHom m : (a : S) → S[M]) x : S[M]) :
          R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
                (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₁ : Eq.{u_2 + 1} (α := R)
  ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
      ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
    R)
  (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
    R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
            ((singleAddHom m : (a : S) → S[M]) x : S[M]) :
          R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
                (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₂ : Eq.{u_2 + 1} (α := R)
  ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) :
    R)
  (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
    R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
            ((singleAddHom m : (a : S) → S[M]) x : S[M]) :
          R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₂ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        (HSMul.hSMul (β := S[M]) c (single m x)) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
                (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₃ : (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) =
  HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MonoidAlgebra.Module (goal)
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddZeroClass M
f : S →+* R
g : MonoidHom.{u_4, u_2} (Multiplicative M) R
c : S
φ : S[M]
m : M
x : S
hfg :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M])
            ((singleAddHom m : (a : S) → S[M]) x) :
          S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
            ((singleAddHom m : (a : S) → S[M]) x : S[M]) :
          R) :
      R)
hfg₁ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        ((((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c : S[M] →+ S[M]) : (a : S[M]) → S[M]) (single m x) : S[M]) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₂ :
  Eq.{u_2 + 1} (α := R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R)
        (HSMul.hSMul (β := S[M]) c (single m x)) :
      R)
    (((AddMonoidHom.mulLeft ((f : (a : S) → R) c) : R →+ R) : (a : R) → R)
        ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R) :
      R)
hfg₃ :
  (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (HSMul.hSMul (β := S[M]) c (single m x)) =
    HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
      ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((AddMonoidHom.comp
            (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R))
              ((smulAddHom S S[M] : (a : S) → S[M] →+ S[M]) c))
            (singleAddHom m) :
          (a : S) → R)
        x :
      R)
    (((AddMonoidHom.comp
              (AddMonoidHom.comp (AddMonoidHom.mulLeft ((f : (a : S) → R) c))
                (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R)))
              (singleAddHom m) :
            S →+ R) :
          (a : S) → R)
        x :
      R)
have hfg₄ : (liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m (c * x)) =
  HMul.hMul (α := R) (β := R) ((f : (a : S) → R) c : R)
    ((liftNC (↑f : S →+ R) (⇑g : (a : Multiplicative M) → R) : (a : S[M]) → R) (single m x) : R)
Tactic: simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]
-- 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 : (∑ 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: simp_rw [mul_apply, sum, ← Finset.sum_product']
-- 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
⊢ (∑ 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)
have refine_1 : ∀ b ∈ f.support ×ˢ 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: refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl)
-- 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
refine_1 :
  ∀ b ∈ f.support ×ˢ 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
⊢ (∑ 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)
have refine_2 : (a0, b0) ∉ f.support ×ˢ g.support →
  (if (a0, b0).1 * (a0, b0).2 = a0 * b0 then
      HMul.hMul (α := R) (β := R) ((f : (a : A) → R) (a0, b0).1 : R) ((g : (a : A) → R) (a0, b0).2 : R)
    else 0) =
    0
Tactic: refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl)
-- 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
⊢ ∀ b ∈ f.support ×ˢ 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
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: simp_rw [Finset.mem_product]
-- 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
⊢ (a0, b0) ∉ f.support ×ˢ g.support →
    (if (a0, b0).1 * (a0, b0).2 = a0 * b0 then
        HMul.hMul (α := R) (β := R) ((f : (a : A) → R) (a0, b0).1 : R) ((g : (a : A) → R) (a0, b0).2 : R)
      else 0) =
      0
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: simp_rw [Finset.mem_product]
-- 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
⊢ ∀ (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
have refine_1 : ∀ (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: refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
-- 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
refine_1 :
  ∀ (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
⊢ ∀ (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
have refine_1₁ : ∀ (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: refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)
-- 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
⊢ ¬(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
have 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
Tactic: refine fun hnotMem ↦ ite_eq_right_iff.mpr (fun _ ↦ ?_)
-- 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
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0
have refine_2 : ∀ (af : a0 ∉ f.support), 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
-- 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
refine_2 :
  ∀ (af : a0 ∉ f.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
have refine_2₁ : ∀ (bg : b0 ∉ g.support), 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
-- 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
af : a0 ∉ f.support
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0
have refine_2 : HMul.hMul (α := R) (β := R) (0 : R) ((g : (a : A) → R) b0 : R) = 0
Tactic: rw [notMem_support_iff.mp af, zero_mul]
-- 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
af : a0 ∉ f.support
refine_2 : HMul.hMul (α := R) (β := R) (0 : 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
have refine_2₁ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [notMem_support_iff.mp af, zero_mul]
-- 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
⊢ HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) ((g : (a : A) → R) b0 : R) = 0
have refine_2 : HMul.hMul (α := R) (β := R) ((f : (a : A) → R) a0 : R) (0 : R) = 0
Tactic: rw [notMem_support_iff.mp bg, mul_zero]