chore: another non-class instance (#7250)

Following #7245, https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/isClass.3F.20panic!/near/391779504.

There is one exception that it is unclear how to fix, it seems lean makes the internal declarations in a block of mutual instances also instances perhaps? Seeing as it is internal I hope it won't cause too much trouble

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -120,7 +120,7 @@ theorem restrictScalars.smul_def' {R : Type u₁} {S : Type u₂} [Ring R] [Ring
 
 instance (priority := 100) sMulCommClass_mk {R : Type u₁} {S : Type u₂} [Ring R] [CommRing S]
     (f : R →+* S) (M : Type v) [I : AddCommGroup M] [Module S M] :
-    have : SMul R M := (RestrictScalars.obj' f (ModuleCat.mk M)).isModule.toSMul
+    haveI : SMul R M := (RestrictScalars.obj' f (ModuleCat.mk M)).isModule.toSMul
     SMulCommClass R S M :=
   -- Porting note: cannot synth SMul R M
   have : SMul R M := (RestrictScalars.obj' f (ModuleCat.mk M)).isModule.toSMul