feat: add Function.Injective.smulCommClass and `Function.Surjective…

….smulCommClass` (#5377)

Mathlib/GroupTheory/GroupAction/Defs.lean

@@ -229,6 +229,18 @@ theorem SMulCommClass.symm (M N α : Type _) [SMul M α] [SMul N α] [SMulCommCl
 because this would cause a loop in the instance search graph. -/
 add_decl_doc VAddCommClass.symm
 
+theorem Function.Injective.smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β]
+    [SMulCommClass M N β] {f : α → β} (hf : Function.Injective f)
+    (h₁ : ∀ (c : M) x, f (c • x) = c • f x) (h₂ : ∀ (c : N) x, f (c • x) = c • f x) :
+    SMulCommClass M N α where
+  smul_comm c₁ c₂ x := hf <| by simp only [h₁, h₂, smul_comm c₁ c₂ (f x)]
+
+theorem Function.Surjective.smulCommClass [SMul M α] [SMul N α] [SMul M β] [SMul N β]
+    [SMulCommClass M N α] {f : α → β} (hf : Function.Surjective f)
+    (h₁ : ∀ (c : M) x, f (c • x) = c • f x) (h₂ : ∀ (c : N) x, f (c • x) = c • f x) :
+    SMulCommClass M N β where
+  smul_comm c₁ c₂ := hf.forall.2 fun x ↦ by simp only [← h₁, ← h₂, smul_comm c₁ c₂ x]
+
 @[to_additive]
 instance smulCommClass_self (M α : Type _) [CommMonoid M] [MulAction M α] : SMulCommClass M M α :=
   ⟨fun a a' b => by rw [← mul_smul, mul_comm, mul_smul]⟩