chore: copy Finsupp.smul_single' to (Add)MonoidAlgebra to avoid…

… defeq abuse (#17825)

This seems to stem from Lean 3 where it was okay to `simp` with `Finsupp` lemmas in its type synonyms `MonoidAlgebra` and `AddMonoidAlgebra`. The discrimination tree in Lean 4 correctly catches the mismatch. So we copy the lemma to the type synonyms and remove some porting notes.

Mathlib/Algebra/MonoidAlgebra/Defs.lean

@@ -477,9 +477,13 @@ def of [MulOneClass G] : G →* MonoidAlgebra k G :=
 
 end
 
+/-- Copy of `Finsupp.smul_single'` that avoids the `MonoidAlgebra = Finsupp` defeq abuse. -/
+@[simp]
+theorem smul_single' (c : k) (a : G) (b : k) : c • single a b = single a (c * b) :=
+  Finsupp.smul_single' c a b
+
 theorem smul_of [MulOneClass G] (g : G) (r : k) : r • of k G g = single g r := by
-  -- porting note (#10745): was `simp`.
-  rw [of_apply, smul_single', mul_one]
+  simp
 
 theorem of_injective [MulOneClass G] [Nontrivial k] :
     Function.Injective (of k G) := fun a b h => by
@@ -671,8 +675,7 @@ theorem induction_on [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f
   refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_
   · simpa using hsmul 0 (of k G 1) (hM 1)
   · convert hsmul r (of k G g) (hM g)
-    -- Porting note: Was `simp only`.
-    rw [of_apply, smul_single', mul_one]
+    simp
 
 section
 
@@ -1223,6 +1226,11 @@ def singleHom [AddZeroClass G] : k × Multiplicative G →* k[G] where
   map_one' := rfl
   map_mul' _a _b := single_mul_single.symm
 
+/-- Copy of `Finsupp.smul_single'` that avoids the `AddMonoidAlgebra = Finsupp` defeq abuse. -/
+@[simp]
+theorem smul_single' (c : k) (a : G) (b : k) : c • single a b = single a (c * b) :=
+  Finsupp.smul_single' c a b
+
 theorem mul_single_apply_aux [Add G] (f : k[G]) (r : k) (x y z : G)
     (H : ∀ a, a + x = z ↔ a = y) : (f * single x r) z = f y * r :=
   @MonoidAlgebra.mul_single_apply_aux k (Multiplicative G) _ _ _ _ _ _ _ H
@@ -1267,8 +1275,7 @@ theorem induction_on [AddMonoid G] {p : k[G] → Prop} (f : k[G])
   refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_
   · simpa using hsmul 0 (of k G (Multiplicative.ofAdd 0)) (hM 0)
   · convert hsmul r (of k G (Multiplicative.ofAdd g)) (hM g)
-    -- Porting note: Was `simp only`.
-    rw [of_apply, toAdd_ofAdd, smul_single', mul_one]
+    simp
 
 /-- If `f : G → H` is an additive homomorphism between two additive monoids, then
 `Finsupp.mapDomain f` is a ring homomorphism between their add monoid algebras. -/

Mathlib/Algebra/MonoidAlgebra/Grading.lean

@@ -132,7 +132,7 @@ theorem decomposeAux_single (m : M) (r : R) :
   refine (DirectSum.of_smul R _ _ _).symm.trans ?_
   apply DirectSum.of_eq_of_gradedMonoid_eq
   refine Sigma.subtype_ext rfl ?_
-  refine (Finsupp.smul_single' _ _ _).trans ?_
+  refine (smul_single' _ _ _).trans ?_
   rw [mul_one]
   rfl
 

Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

@@ -214,35 +214,20 @@ theorem diagonalSucc_inv_single_left (g : G) (f : Gⁿ →₀ k) (r : k) :
     (diagonalSucc k G n).inv.hom (Finsupp.single g r ⊗ₜ f) =
       Finsupp.lift (Gⁿ⁺¹ →₀ k) k Gⁿ (fun f => single (g • partialProd f) r) f := by
   refine f.induction ?_ ?_
-/- Porting note (#11039): broken proof was
   · simp only [TensorProduct.tmul_zero, map_zero]
-  · intro a b x ha hb hx
+  · intro a b x _ _ hx
     simp only [lift_apply, smul_single', mul_one, TensorProduct.tmul_add, map_add,
       diagonalSucc_inv_single_single, hx, Finsupp.sum_single_index, mul_comm b,
-      zero_mul, single_zero] -/
-  · rw [TensorProduct.tmul_zero, map_zero]
-    rw [map_zero]
-  · intro _ _ _ _ _ hx
-    rw [TensorProduct.tmul_add, map_add, map_add, hx]
-    simp_rw [lift_apply, smul_single, smul_eq_mul]
-    rw [diagonalSucc_inv_single_single, sum_single_index, mul_comm]
-    rw [zero_mul, single_zero]
+      zero_mul, single_zero]
 
 theorem diagonalSucc_inv_single_right (g : G →₀ k) (f : Gⁿ) (r : k) :
     (diagonalSucc k G n).inv.hom (g ⊗ₜ Finsupp.single f r) =
       Finsupp.lift _ k G (fun a => single (a • partialProd f) r) g := by
   refine g.induction ?_ ?_
-/- Porting note (#11039): broken proof was
   · simp only [TensorProduct.zero_tmul, map_zero]
-  · intro a b x ha hb hx
+  · intro a b x _ _ hx
     simp only [lift_apply, smul_single', map_add, hx, diagonalSucc_inv_single_single,
-      TensorProduct.add_tmul, Finsupp.sum_single_index, zero_mul, single_zero] -/
-  · rw [TensorProduct.zero_tmul, map_zero, map_zero]
-  · intro _ _ _ _ _ hx
-    rw [TensorProduct.add_tmul, map_add, map_add, hx]
-    simp_rw [lift_apply, smul_single']
-    rw [diagonalSucc_inv_single_single, sum_single_index]
-    rw [zero_mul, single_zero]
+      TensorProduct.add_tmul, Finsupp.sum_single_index, zero_mul, single_zero]
 
 end Rep