feat(Algebra/MonoidAlgebra): when single and of commute (#8975)

Also removes an `autoImplicit` that tripped me up when working on this file.

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -50,8 +50,6 @@ Similarly, I attempted to just define
 `Multiplicative G = G` leaks through everywhere, and seems impossible to use.
 -/
 
-set_option autoImplicit true
-
 
 noncomputable section
 
@@ -118,7 +116,8 @@ theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b
   Finsupp.single_add a b₁ b₂
 
 @[simp]
-theorem sum_single_index [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) :
+theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N}
+    (h_zero : h a 0 = 0) :
     (single a b).sum h = h a b := Finsupp.sum_single_index h_zero
 
 @[simp]
@@ -452,6 +451,17 @@ theorem single_mul_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} :
     (sum_single_index (by rw [mul_zero, single_zero]))
 #align monoid_algebra.single_mul_single MonoidAlgebra.single_mul_single
 
+theorem single_commute_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k}
+    (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
+    Commute (single a₁ b₁) (single a₂ b₂) :=
+  single_mul_single.trans <| congr_arg₂ single ha hb |>.trans single_mul_single.symm
+
+theorem single_commute [Mul G] {a : G} {b : k} (ha : ∀ a', Commute a a') (hb : ∀ b', Commute b b') :
+    ∀ f : MonoidAlgebra k G, Commute (single a b) f :=
+  suffices AddMonoidHom.mulLeft (single a b) = AddMonoidHom.mulRight (single a b) from
+    FunLike.congr_fun this
+  addHom_ext' fun a' => AddMonoidHom.ext fun b' => single_commute_single (ha a') (hb b')
+
 @[simp]
 theorem single_pow [Monoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (a ^ n) (b ^ n)
   | 0 => by
@@ -516,6 +526,10 @@ theorem of_injective [MulOneClass G] [Nontrivial k] :
   simpa using (single_eq_single_iff _ _ _ _).mp h
 #align monoid_algebra.of_injective MonoidAlgebra.of_injective
 
+theorem of_commute [MulOneClass G] {a : G} (h : ∀ a', Commute a a') (f : MonoidAlgebra k G) :
+    Commute (of k G a) f :=
+  single_commute h Commute.one_left f
+
 /-- `Finsupp.single` as a `MonoidHom` from the product type into the monoid algebra.
 
 Note the order of the elements of the product are reversed compared to the arguments of
@@ -729,10 +743,8 @@ section Algebra
 -- attribute [local reducible] MonoidAlgebra -- Porting note: `reducible` cannot be `local`.
 
 theorem single_one_comm [CommSemiring k] [MulOneClass G] (r : k) (f : MonoidAlgebra k G) :
-    single (1 : G) r * f = f * single (1 : G) r := by
-  -- Porting note: `ext` → `refine Finsupp.ext fun _ => ?_`
-  refine Finsupp.ext fun _ => ?_
-  rw [single_one_mul_apply, mul_single_one_apply, mul_comm]
+    single (1 : G) r * f = f * single (1 : G) r :=
+  single_commute Commute.one_left (Commute.all _) f
 #align monoid_algebra.single_one_comm MonoidAlgebra.single_one_comm
 
 /-- `Finsupp.single 1` as a `RingHom` -/
@@ -1235,7 +1247,8 @@ theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b
   Finsupp.single_add a b₁ b₂
 
 @[simp]
-theorem sum_single_index [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) :
+theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N}
+    (h_zero : h a 0 = 0) :
     (single a b).sum h = h a b := Finsupp.sum_single_index h_zero
 
 @[simp]
@@ -1554,6 +1567,11 @@ theorem single_mul_single [Add G] {a₁ a₂ : G} {b₁ b₂ : k} :
   @MonoidAlgebra.single_mul_single k (Multiplicative G) _ _ _ _ _ _
 #align add_monoid_algebra.single_mul_single AddMonoidAlgebra.single_mul_single
 
+theorem single_commute_single [Add G] {a₁ a₂ : G} {b₁ b₂ : k}
+    (ha : AddCommute a₁ a₂) (hb : Commute b₁ b₂) :
+    Commute (single a₁ b₁) (single a₂ b₂) :=
+  @MonoidAlgebra.single_commute_single k (Multiplicative G) _ _ _ _ _ _ ha hb
+
 -- This should be a `@[simp]` lemma, but the simp_nf linter times out if we add this.
 -- Probably the correct fix is to make a `[Add]MonoidAlgebra.single` with the correct type,
 -- instead of relying on `Finsupp.single`.
@@ -1632,6 +1650,11 @@ theorem of_injective [Nontrivial k] [AddZeroClass G] : Function.Injective (of k
   MonoidAlgebra.of_injective
 #align add_monoid_algebra.of_injective AddMonoidAlgebra.of_injective
 
+theorem of'_commute [Semiring k] [AddZeroClass G] {a : G} (h : ∀ a', AddCommute a a')
+    (f : AddMonoidAlgebra k G) :
+    Commute (of' k G a) f :=
+  MonoidAlgebra.of_commute (G := Multiplicative G) h f
+
 /-- `Finsupp.single` as a `MonoidHom` from the product type into the additive monoid algebra.
 
 Note the order of the elements of the product are reversed compared to the arguments of