chore: fix non-reducible diamonds around scalar multiplication in RingCon (leanprover-community#40704)

The following fails before the PR, succeeds after it.
```
example {R : Type*} [Ring R] (c : RingCon R) :
    (RingCon.hasZSMul c : SMul ℤ c.Quotient) = RingCon.instSMulQuotient c := by
  with_reducible_and_instances rfl -- fails
```

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/RingTheory/Congruence/Basic.lean

@@ -52,7 +52,7 @@ variable [SMul α R] [IsScalarTower α R R]
 variable [SMul β R] [IsScalarTower β R R]
 variable (c : RingCon R)
 
-instance : SMul α c.Quotient := inferInstanceAs (SMul α c.toCon.Quotient)
+instance : SMul α c.Quotient := ⟨c.smulAux (Con.smul c.toCon)⟩
 
 @[simp, norm_cast]
 theorem coe_smul (a : α) (x : R) : (↑(a • x) : c.Quotient) = a • (x : c.Quotient) :=

Mathlib/RingTheory/Congruence/Defs.lean

@@ -252,6 +252,13 @@ theorem coe_one : (↑(1 : R) : c.Quotient) = 1 :=
 
 end One
 
+/-- A function used to define scalar actions on `RingCon.Quotient`. To make sure such actions coming
+from different sources are reducibly defeq, they should all go through this function. -/
+def smulAux [Add R] [Mul R] {α : Type*} [SMul α R]
+    (c : RingCon R) (h : ∀ (a : α) (x y : R), c x y → c (a • x) (a • y))
+    (a : α) (x : c.Quotient) : c.Quotient :=
+  Quotient.map' (a • ·) (h a) x
+
 section NegSubZSMul
 
 variable [AddGroup R] [Mul R] (c : RingCon R)
@@ -268,7 +275,7 @@ instance : Sub c.Quotient := inferInstanceAs (Sub c.toAddCon.Quotient)
 theorem coe_sub (x y : R) : (↑(x - y) : c.Quotient) = x - y :=
   rfl
 
-instance hasZSMul : SMul ℤ c.Quotient := inferInstanceAs (SMul ℤ c.toAddCon.Quotient)
+instance hasZSMul : SMul ℤ c.Quotient := ⟨c.smulAux (RingCon.zsmul c)⟩
 
 @[simp, norm_cast]
 theorem coe_zsmul (z : ℤ) (x : R) : (↑(z • x) : c.Quotient) = z • (x : c.Quotient) :=
@@ -280,7 +287,7 @@ section NSMul
 
 variable [AddMonoid R] [Mul R] (c : RingCon R)
 
-instance hasNSMul : SMul ℕ c.Quotient := inferInstanceAs (SMul ℕ c.toAddCon.Quotient)
+instance hasNSMul : SMul ℕ c.Quotient := ⟨c.smulAux (RingCon.nsmul c)⟩
 
 @[simp, norm_cast]
 theorem coe_nsmul (n : ℕ) (x : R) : (↑(n • x) : c.Quotient) = n • (x : c.Quotient) :=
@@ -353,14 +360,16 @@ instance [AddCommMagma R] [Mul R] (c : RingCon R) : AddCommMagma c.Quotient :=
 instance [AddCommSemigroup R] [Mul R] (c : RingCon R) : AddCommSemigroup c.Quotient :=
   inferInstanceAs <| AddCommSemigroup c.toAddCon.Quotient
 
-instance [AddMonoid R] [Mul R] (c : RingCon R) : AddMonoid c.Quotient :=
-  inferInstanceAs <| AddMonoid c.toAddCon.Quotient
+instance [AddMonoid R] [Mul R] (c : RingCon R) : AddMonoid c.Quotient where
+  nsmul n x := n • x
+  __ : AddMonoid c.Quotient := inferInstanceAs <| AddMonoid c.toAddCon.Quotient
 
 instance [AddCommMonoid R] [Mul R] (c : RingCon R) : AddCommMonoid c.Quotient :=
   inferInstanceAs <| AddCommMonoid c.toAddCon.Quotient
 
-instance [AddGroup R] [Mul R] (c : RingCon R) : AddGroup c.Quotient :=
-  inferInstanceAs <| AddGroup c.toAddCon.Quotient
+instance [AddGroup R] [Mul R] (c : RingCon R) : AddGroup c.Quotient where
+  zsmul n x := n • x
+  __ : AddGroup c.Quotient := inferInstanceAs <| AddGroup c.toAddCon.Quotient
 
 instance [AddCommGroup R] [Mul R] (c : RingCon R) : AddCommGroup c.Quotient :=
   inferInstanceAs <| AddCommGroup c.toAddCon.Quotient