feat: clean up Mul -> FaithfulSMul instance structure (#34789)

Given `MulOneClass A`, the induced smultiplications `SMul A A` and `SMul (MulOpposite A) A` are faithful. As a result, the same holds when given `RightCancelMonoid A`, `LeftCancelMonoid A` or `RightCancelMonoidWithZero A`. the instances representing the latter three facts are removed due to their redundancy. (Also for the `to_additive` versions when applicable.)

Secondly, given `Mul A`, and given `IsRightCancelMul A` or `IsLeftCancelMul A`, we find that `SMul A A` or `SMul (MulOpposite A) A` is faithful, respectively. The instances representing these facts are added.

Co-authored-by: Edward van de Meent <edwardvdmeent@gmail.com>

Author: edegeltje

Mathlib/Algebra/Group/Action/Faithful.lean

@@ -55,20 +55,46 @@ export FaithfulVAdd (eq_of_vadd_eq_vadd)
 lemma smul_left_injective' [SMul M α] [FaithfulSMul M α] : Injective ((· • ·) : M → α → α) :=
   fun _ _ h ↦ FaithfulSMul.eq_of_smul_eq_smul (congr_fun h)
 
+/-- `instSMulOfMul` is faithful when there is a (right) identity. -/
+@[to_additive /-- `instVAddOfAdd` is faithful when there is a (right) identity. -/]
+instance (R : Type*) [MulOneClass R] : FaithfulSMul R R where
+  eq_of_smul_eq_smul {r₁ r₂} h := by simpa using h 1
+
+/-- `Mul.toSMulMulOpposite` is faithful when there is a (left) identity. -/
+@[to_additive /-- `Add.toVAddAddOpposite` is faithful when there is a (left) identity. -/]
+instance (R : Type*) [MulOneClass R] : FaithfulSMul Rᵐᵒᵖ R where
+  eq_of_smul_eq_smul {r₁ r₂} h := by simpa using h 1
+
+/-- `instSMulOfMul` is faithful when multiplication is right cancellative. -/
+@[to_additive /-- `instVAddOfAdd` is faithful when addition is right cancellative. -/]
+instance (R : Type*) [Mul R] [IsRightCancelMul R] : FaithfulSMul R R where
+  eq_of_smul_eq_smul {r₁ r₂} h := by simpa using h r₁
+
+/-- `Mul.toSMulMulOpposite` is faithful when multiplication is left cancellative -/
+@[to_additive /-- `Add.toVAddAddOpposite` is faithful when addition is left cancellative -/]
+instance (R : Type*) [Mul R] [IsLeftCancelMul R] : FaithfulSMul Rᵐᵒᵖ R where
+  eq_of_smul_eq_smul {r₁ r₂} h := by simpa using h r₁.unop
+
 /-- `Monoid.toMulAction` is faithful on cancellative monoids. -/
-@[to_additive /-- `AddMonoid.toAddAction` is faithful on additive cancellative monoids. -/]
-instance RightCancelMonoid.faithfulSMul [RightCancelMonoid α] : FaithfulSMul α α :=
-  ⟨fun h ↦ mul_right_cancel (h 1)⟩
+@[to_additive (attr :=
+  deprecated "subsumed by `instFaithfulSMul` or `instFaithfulSMulOfIsRightCancelMul`"
+  (since := "2026-02-03"))
+  /-- `AddMonoid.toAddAction` is faithful on additive cancellative monoids. -/]
+lemma RightCancelMonoid.faithfulSMul [RightCancelMonoid α] : FaithfulSMul α α :=
+  inferInstance
 
 /-- `Monoid.toOppositeMulAction` is faithful on cancellative monoids. -/
-@[to_additive /-- `AddMonoid.toOppositeAddAction` is faithful on additive cancellative monoids. -/]
-instance LeftCancelMonoid.to_faithfulSMul_mulOpposite [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α :=
-  ⟨fun h ↦ MulOpposite.unop_injective <| mul_left_cancel (h 1)⟩
+@[to_additive (attr :=
+    deprecated "subsumed by `instFaithfulSMulMulOpposite` or \
+    `instFaithfulSMulMulOppositeOfIsLeftCancelMul`"
+    (since := "2026-02-03"))
+  /-- `AddMonoid.toOppositeAddAction` is faithful on additive cancellative monoids. -/]
+lemma LeftCancelMonoid.to_faithfulSMul_mulOpposite [LeftCancelMonoid α] : FaithfulSMul αᵐᵒᵖ α :=
+  inferInstance
 
 @[deprecated (since := "2025-09-15")]
 alias LefttCancelMonoid.to_faithfulSMul_mulOpposite := LeftCancelMonoid.to_faithfulSMul_mulOpposite
 
-instance (R : Type*) [MulOneClass R] : FaithfulSMul R R := ⟨fun {r₁ r₂} h ↦ by simpa using h 1⟩
 
 @[to_additive]
 lemma faithfulSMul_iff_injective_smul_one (R A : Type*)

Mathlib/Algebra/GroupWithZero/Action/Faithful.lean

@@ -7,10 +7,12 @@ module
 
 public import Mathlib.Algebra.Group.Action.Faithful
 public import Mathlib.Algebra.GroupWithZero.NeZero
+public import Mathlib.Tactic.Linter.DeprecatedModule
 
 /-!
 # Faithful actions involving groups with zero
 -/
+deprecated_module (since := "2026-02-03")
 
 @[expose] public section
 
@@ -21,9 +23,6 @@ open Function
 variable {α : Type*}
 
 /-- `Monoid.toMulAction` is faithful on nontrivial cancellative monoids with zero. -/
-instance IsRightCancelMulZero.faithfulSMul [MonoidWithZero α] [IsRightCancelMulZero α] :
-    FaithfulSMul α α where
-  eq_of_smul_eq_smul h := by
-    cases subsingleton_or_nontrivial α
-    · exact Subsingleton.elim ..
-    · exact mul_left_injective₀ one_ne_zero (h 1)
+@[nolint unusedArguments, deprecated "subsumed by `instFaithfulSMul`" (since := "2026-02-03")]
+lemma IsRightCancelMulZero.faithfulSMul [MonoidWithZero α] [IsRightCancelMulZero α] :
+    FaithfulSMul α α := inferInstance