fix(RingTheory/TwoSidedIdeal/Basic): remove instance with bad outParam (#40718)

There are two different instances for `SMulMemClass (TwoSidedIdeal R) _ R`, which violates the fact the fact that the second argument in the class is an `outParam` . So, this PR turns one of the instances into just a theorem.

Author: JovanGerb

Mathlib/RingTheory/TwoSidedIdeal/Basic.lean

@@ -192,7 +192,10 @@ lemma coe_mk' (carrier : Set R) (zero_mem add_mem neg_mem mul_mem_left mul_mem_r
 instance : SMulMemClass (TwoSidedIdeal R) R R where
   smul_mem _ _ h := TwoSidedIdeal.mul_mem_left _ _ _ h
 
-instance : SMulMemClass (TwoSidedIdeal R) Rᵐᵒᵖ R where
+-- This is not an instance, because together with the instance above,
+-- it violates the `outParam` of `SMulMemClass`.
+-- See: https://github.com/leanprover-community/mathlib4/pull/40718
+theorem instSMulMemClassMulOpposite : SMulMemClass (TwoSidedIdeal R) Rᵐᵒᵖ R where
   smul_mem _ _ h := TwoSidedIdeal.mul_mem_right _ _ _ h
 
 instance : Add I where add x y := ⟨x.1 + y.1, I.add_mem x.2 y.2⟩