fix: CompatibleSMul : Prop (#6065)

Lean makes it `Type` otherwise. Why does this happen? Am I missing something?

Mathlib/Algebra/Module/LinearMap.lean

@@ -399,7 +399,7 @@ we can also add an instance for `AddCommGroup.intModule`, allowing `z •` to be
 `R` does not support negation.
 -/
 class CompatibleSMul (R S : Type _) [Semiring S] [SMul R M] [Module S M] [SMul R M₂]
-  [Module S M₂] where
+  [Module S M₂] : Prop where
   /-- Scalar multiplication by `R` of `M` can be moved through linear maps. -/
   map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c • x) = c • fₗ x
 #align linear_map.compatible_smul LinearMap.CompatibleSMul