awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : MulOneClass M
f : S →+* R
g : M →* R
c : S
φ : S[M]
hfg :
  ∀ (m : M) (x : S),
    Eq.{u_2 + 1} (α := R)
      ((AddMonoidHom.comp
              (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : 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 : M) → R)))
                (singleAddHom m) :
              S →+ R) :
            (a : S) → R)
          x :
        R)
⊢ Eq (α := S[M] →+ R)
    (AddMonoidHom.comp (N := S[M]) (liftNC (↑f : S →+ R) (⇑g : (a : 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 : M) → R)))

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : IsScalarTower R k k
t : R
a b : k[G]
hfg : ∀ (m : G), Eq.{u₁ + 1} (α := k) (((t • a) • b : (a : G) → k) m : k) ((t • a • b : (a : G) → k) m : k)
⊢ (t • a) • b = t • a • b

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : IsScalarTower R k k
t : R
a b : k[G]
m : G
⊢ Eq.{u₁ + 1} (α := k) (((t • a) • b : (a : G) → k) m : k) ((t • a • b : (a : G) → k) m : k)

Tactic:
simp [mul_apply, sum_smul_index' (b := t), smul_sum, smul_mul_assoc]

Premises used: Finsupp.sum_smul_index', smul_mul_assoc, MonoidAlgebra.mul_apply, Finsupp.smul_sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : IsScalarTower R k k
t : R
a b : k[G]
hfg hfg₁ : ∀ (m : G), Eq.{u₁ + 1} (α := k) (((t • a) • b : (a : G) → k) m : k) ((t • a • b : (a : G) → k) m : k)
⊢ (t • a) • b = t • a • b

Tactic:
classical ext; simp [mul_apply, sum_smul_index' (b := t), smul_sum, smul_mul_assoc]

Premises used: Finsupp.sum_smul_index', smul_mul_assoc, MonoidAlgebra.mul_apply, Finsupp.smul_sum
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
hfg : ∀ (m : G), Eq.{u₁ + 1} (α := k) ((t • a • b : (a : G) → k) m : k) ((a • t • b : (a : G) → k) m : k)
⊢ t • a • b = a • t • b

Tactic:
ext
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
hfg :
  Eq (α := k) ((t • (a * b) : (a : G) → k) m : k)
    (sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : k)
⊢ Eq.{u₁ + 1} (α := k) ((t • a • b : (a : G) → k) m : k) ((a • t • b : (a : G) → k) m : k)

Tactic:
simp only [smul_eq_mul, mul_apply]

Premises used: MonoidAlgebra.mul_apply, smul_eq_mul
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
hfg :
  HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
    sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
⊢ Eq (α := k) ((t • (a * b) : (a : G) → k) m : k)
    (sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : k)

Tactic:
rw [coe_smul]

Premises used: Finsupp.coe_smul
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
⊢ HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
    sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0

Tactic:
Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_)

Premises used: Finsupp.sum_smul_index', Finsupp.sum, congr_arg, funext₂, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
hfg : ∀ (a₁ : G) (b₁ : k) (i : G), (if a₁ * i = m then b₁ * 0 else 0) = 0
hfg₁ :
  (sum a fun (a₁ : G) (b₁ : k) ↦ sum b fun (i : G) (c : k) ↦ if a₁ * i = m then b₁ * t • c else 0) =
    HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m
⊢ HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
    sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0

Tactic:
refine Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_)

Premises used: Finsupp.sum_smul_index', Finsupp.sum, congr_arg, funext₂, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m a₁ : G
b₁ : k
⊢ ∀ (i : G), (if a₁ * i = m then b₁ * 0 else 0) = 0

Tactic:
simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm,
      imp_true_iff, ite_eq_right_iff, Pi.smul_apply, mul_zero, smul_zero]

Premises used: Finsupp.sum, smul_zero, MulZeroClass.mul_zero, imp_true_iff, smul_ite, ite_eq_right_iff, MonoidAlgebra.mul_apply, Finset.smul_sum, mul_smul_comm, Pi.smul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
⊢ (sum a fun (a₁ : G) (b₁ : k) ↦ sum b fun (i : G) (c : k) ↦ if a₁ * i = m then b₁ * t • c else 0) =
    HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m

Tactic:
simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm,
      imp_true_iff, ite_eq_right_iff, Pi.smul_apply, mul_zero, smul_zero]

Premises used: Finsupp.sum, smul_zero, MulZeroClass.mul_zero, imp_true_iff, smul_ite, ite_eq_right_iff, MonoidAlgebra.mul_apply, Finset.smul_sum, mul_smul_comm, Pi.smul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass R k k
t : R
a b : k[G]
m : G
hfg :
  Eq (α := k) ((t • (a * b) : (a : G) → k) m : k)
    (sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0 : k)
hfg₁ :
  HSMul.hSMul (β := (a : G) → k) t (⇑(a * b) : (a : G) → k) m =
    sum a fun (m₁ : G) (r₁ : k) ↦ sum (t • b) fun (m₂ : G) (r₂ : k) ↦ if m₁ * m₂ = m then r₁ * r₂ else 0
⊢ Eq.{u₁ + 1} (α := k) ((t • a • b : (a : G) → k) m : k) ((a • t • b : (a : G) → k) m : k)

Tactic:
classical
    simp only [smul_eq_mul, mul_apply]
    rw [coe_smul]
    refine Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_) <;>
    simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm,
      imp_true_iff, ite_eq_right_iff, Pi.smul_apply, mul_zero, smul_zero]

Premises used: Finsupp.sum_smul_index', Finsupp.sum, smul_zero, MulZeroClass.mul_zero, imp_true_iff, congr_arg, smul_ite, Finsupp.coe_smul, ite_eq_right_iff, funext₂, MonoidAlgebra.mul_apply, Finset.smul_sum, mul_smul_comm, smul_eq_mul, Eq.symm, Eq.trans, Pi.smul_apply
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : Semiring k
inst_1 : DistribSMul R k
inst_2 : Mul G
inst_3 : SMulCommClass k R k
⊢ SMulCommClass k[G] R k[G]

Tactic:
have := SMulCommClass.symm k R k; .symm ..

Premises used: SMulCommClass.symm, MonoidAlgebra
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
V : Type u_5
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) v ∈ W
f : k[G]
v : V
hv : v ∈ (↑W : Set V)
rw : ∑ i ∈ f.support, HSMul.hSMul (α := k[G]) (Finsupp.single i ((f : (a : G) → k) i) : G →₀ k) v ∈ (↑W : Set V)
⊢ f • v ∈ (↑W : Set V)

Tactic:
rw [← Finsupp.sum_single f, Finsupp.sum, Finset.sum_smul]

Premises used: Finset.sum_smul, Finsupp.sum, Finsupp.sum_single
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
V : Type u_5
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) v ∈ W
f : k[G]
v : V
hv : v ∈ (↑W : Set V)
simp_rw :
  ∑ x ∈ f.support,
      HSMul.hSMul.{u₁, u_5, u_5} (α := k) ((f : (a : G) → k) x : k)
        (HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) x : k[G]) v) ∈
    (↑W : Set V)
⊢ ∑ i ∈ f.support, HSMul.hSMul (α := k[G]) (Finsupp.single i ((f : (a : G) → k) i) : G →₀ k) v ∈ (↑W : Set V)

Tactic:
simp_rw [← smul_of, smul_assoc]

Premises used: smul_assoc, MonoidAlgebra.smul_of
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
V : Type u_5
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) v ∈ W
f : k[G]
v : V
hv : v ∈ (↑W : Set V)
⊢ ∑ x ∈ f.support,
      HSMul.hSMul.{u₁, u_5, u_5} (α := k) ((f : (a : G) → k) x : k)
        (HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) x : k[G]) v) ∈
    (↑W : Set V)

Tactic:
Submodule.sum_smul_mem W _ fun g _ => h g v hv

Premises used: Submodule.sum_smul_mem
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
k : Type u₁
G : Type u₂
H : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
inst : CommSemiring k
inst_1 : Monoid G
V : Type u_5
inst_2 : AddCommMonoid V
inst_3 : Module k V
inst_4 : Module k[G] V
inst_5 : IsScalarTower k k[G] V
W : Submodule k V
h : ∀ (g : G), ∀ v ∈ W, HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) g : k[G]) v ∈ W
f : k[G]
v : V
hv : v ∈ (↑W : Set V)
⊢ ∑ x ∈ f.support,
      HSMul.hSMul.{u₁, u_5, u_5} (α := k) ((f : (a : G) → k) x : k)
        (HSMul.hSMul (α := k[G]) ((of k G : (a : G) → k[G]) x : k[G]) v) ∈
    (↑W : Set V)

Tactic:
exact Submodule.sum_smul_mem W _ fun g _ => h g v hv

Premises used: Submodule.sum_smul_mem
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : Nontrivial R
m : M
s : Set M
⊢ Membership.mem (γ := Submodule R R[M]) (Submodule.span R (of' R M '' s)) (of' R M m) ↔ m ∈ s

Tactic:
single_mem_span_single _

Premises used: Set.Mem, setOf, Finsupp.single_mem_span_single, AddMonoidAlgebra, AddMonoidAlgebra.of', Finsupp.single
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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)
this :
  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)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure s) m

Tactic:
simpa [← AddSubmonoid.toSubmonoid_closure]

Premises used: AddSubmonoid.toSubmonoid_closure
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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)
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)
⊢ Membership.mem (γ := AddSubmonoid M) (AddSubmonoid.closure s) m

Tactic:
suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' s) by
    simpa [← AddSubmonoid.toSubmonoid_closure]
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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
⊢ 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 _ _
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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))
⊢ 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

Premises used: Set.image_congr', AddMonoidAlgebra.of'_eq_of
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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))
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)
⊢ let s' : Submonoid (Multiplicative M) := Submonoid.closure s;
  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:
rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h

Premises used: Set.image_congr', AddMonoidAlgebra.of'_eq_of
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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
s' : Submonoid (Multiplicative M) := Submonoid.closure s
h :
  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)
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)

Tactic:
simpa using of'_mem_span.1 h

Premises used: AddMonoidAlgebra.of'_mem_span, Iff.mp
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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]
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)))
⊢ (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)

Tactic:
suffices (liftNC (↑f) g).comp (smulAddHom S S[M] c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC f g) from DFunLike.congr_fun this φ
-- Module: Mathlib.Algebra.MonoidAlgebra.Module
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]
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)
⊢ 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:
ext
-- 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 :
  (∑ 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)

Tactic:
simp_rw [mul_apply, sum, ← Finset.sum_product']

Premises used: Finsupp.sum, Finset.sum_product', MonoidAlgebra.mul_apply
-- 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
⊢ (∑ 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:
(Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl)

Premises used: Prod.mk, if_pos, Finset.sum_eq_single, rfl, Eq.trans
-- 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_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
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
⊢ (∑ 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:
refine (Finset.sum_eq_single (a0, b0) ?_ ?_).trans (if_pos rfl)

Premises used: Prod.mk, if_pos, Finset.sum_eq_single, rfl, Eq.trans
-- 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_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
⊢ ∀ 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:
simp_rw [Finset.mem_product]

Premises used: Finset.mem_product
-- 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 :
  ¬(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
⊢ (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:
simp_rw [Finset.mem_product]

Premises used: Finset.mem_product
-- 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
⊢ ∀ (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:
fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)

Premises used: Prod.ext, if_neg
-- 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_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
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
⊢ ∀ (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:
refine fun ab hab hne ↦ if_neg (fun he ↦ hne <| Prod.ext ?_ ?_)

Premises used: if_neg
-- 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:
(h hab.1 hab.2 he).1

Premises used: And.right, And.left