feat(ring_theory/submonoid/membership): generalize a few lemmas to `m…

…ul_mem_class` (#13748)

This generalizes lemmas relating to the additive closure of a multiplicative monoid so that they also apply to multiplicative semigroups using `mul_mem_class`

src/group_theory/submonoid/membership.lean

@@ -457,20 +457,21 @@ attribute [to_additive add_submonoid.multiples_subset] submonoid.powers_subset
 
 end add_submonoid
 
-/-! Lemmas about additive closures of `submonoid`. -/
-namespace submonoid
+/-! Lemmas about additive closures of `subsemigroup`. -/
+namespace mul_mem_class
 
-variables {R : Type*} [non_assoc_semiring R] (S : submonoid R) {a b : R}
+variables {R : Type*} [non_unital_non_assoc_semiring R] [set_like M R] [mul_mem_class M R]
+  {S : M} {a b : R}
 
-/-- The product of an element of the additive closure of a multiplicative submonoid `M`
+/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
 and an element of `M` is contained in the additive closure of `M`. -/
 lemma mul_right_mem_add_closure
   (ha : a ∈ add_submonoid.closure (S : set R)) (hb : b ∈ S) :
   a * b ∈ add_submonoid.closure (S : set R) :=
 begin
   revert b,
   refine add_submonoid.closure_induction ha _ _ _; clear ha a,
-  { exact λ r hr b hb, add_submonoid.mem_closure.mpr (λ y hy, hy (S.mul_mem hr hb)) },
+  { exact λ r hr b hb, add_submonoid.mem_closure.mpr (λ y hy, hy (mul_mem hr hb)) },
   { exact λ b hb, by simp only [zero_mul, (add_submonoid.closure (S : set R)).zero_mem] },
   { simp_rw add_mul,
     exact λ r s hr hs b hb, (add_submonoid.closure (S : set R)).add_mem (hr hb) (hs hb) }
@@ -484,7 +485,7 @@ lemma mul_mem_add_closure
 begin
   revert a,
   refine add_submonoid.closure_induction hb _ _ _; clear hb b,
-  { exact λ r hr b hb, S.mul_right_mem_add_closure hb hr },
+  { exact λ r hr b hb, mul_mem_class.mul_right_mem_add_closure hb hr },
   { exact λ b hb, by simp only [mul_zero, (add_submonoid.closure (S : set R)).zero_mem] },
   { simp_rw mul_add,
     exact λ r s hr hs b hb, (add_submonoid.closure (S : set R)).add_mem (hr hb) (hs hb) }
@@ -494,7 +495,11 @@ end
 submonoid `S` is contained in the additive closure of `S`. -/
 lemma mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ add_submonoid.closure (S : set R)) :
   a * b ∈ add_submonoid.closure (S : set R) :=
-S.mul_mem_add_closure (add_submonoid.mem_closure.mpr (λ sT hT, hT ha)) hb
+mul_mem_add_closure (add_submonoid.mem_closure.mpr (λ sT hT, hT ha)) hb
+
+end mul_mem_class
+
+namespace submonoid
 
 /-- An element is in the closure of a two-element set if it is a linear combination of those two
 elements. -/

src/ring_theory/subsemiring/basic.lean

@@ -582,7 +582,7 @@ namespace submonoid
 /-- The additive closure of a submonoid is a subsemiring. -/
 def subsemiring_closure (M : submonoid R) : subsemiring R :=
 { one_mem' := add_submonoid.mem_closure.mpr (λ y hy, hy M.one_mem),
-  mul_mem' := λ x y, M.mul_mem_add_closure,
+  mul_mem' := λ x y, mul_mem_class.mul_mem_add_closure,
   ..add_submonoid.closure (M : set R)}
 
 lemma subsemiring_closure_coe :