feat: Linter that checks that Prop classes are Props (#6148)

fpvandoorn · fpvandoorn · commit 930dd29d188c · 2023-07-27T15:45:35.000Z
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2987,6 +2987,7 @@ import Mathlib.Tactic.Linarith.Parsing
 import Mathlib.Tactic.Linarith.Preprocessing
 import Mathlib.Tactic.Linarith.Verification
 import Mathlib.Tactic.LinearCombination
+import Mathlib.Tactic.Lint
 import Mathlib.Tactic.Measurability
 import Mathlib.Tactic.Measurability.Init
 import Mathlib.Tactic.MkIffOfInductiveProp
diff --git a/Mathlib/Algebra/Homology/Exact.lean b/Mathlib/Algebra/Homology/Exact.lean
@@ -355,7 +355,7 @@ variable [HasImages W] [HasZeroMorphisms W] [HasKernels W]
 
 /-- A functor reflects exact sequences if any composable pair of morphisms that is mapped to an
     exact pair is itself exact. -/
-class ReflectsExactSequences (F : V ⥤ W) where
+class ReflectsExactSequences (F : V ⥤ W) : Prop where
   reflects : ∀ {A B C : V} (f : A ⟶ B) (g : B ⟶ C), Exact (F.map f) (F.map g) → Exact f g
 #align category_theory.functor.reflects_exact_sequences CategoryTheory.Functor.ReflectsExactSequences
 
diff --git a/Mathlib/Algebra/Jordan/Basic.lean b/Mathlib/Algebra/Jordan/Basic.lean
@@ -77,7 +77,7 @@ Non-commutative Jordan algebras have connections to the Vidav-Palmer theorem
 variable (A : Type _)
 
 /-- A (non-commutative) Jordan multiplication. -/
-class IsJordan [Mul A] where
+class IsJordan [Mul A] : Prop where
   lmul_comm_rmul : ∀ a b : A, a * b * a = a * (b * a)
   lmul_lmul_comm_lmul : ∀ a b : A, a * a * (a * b) = a * (a * a * b)
   lmul_lmul_comm_rmul : ∀ a b : A, a * a * (b * a) = a * a * b * a
@@ -86,7 +86,7 @@ class IsJordan [Mul A] where
 #align is_jordan IsJordan
 
 /-- A commutative Jordan multipication -/
-class IsCommJordan [Mul A] where
+class IsCommJordan [Mul A] : Prop where
   mul_comm : ∀ a b : A, a * b = b * a
   lmul_comm_rmul_rmul : ∀ a b : A, a * b * (a * a) = a * (b * (a * a))
 #align is_comm_jordan IsCommJordan
diff --git a/Mathlib/Algebra/Lie/Basic.lean b/Mathlib/Algebra/Lie/Basic.lean
@@ -90,7 +90,7 @@ class LieRingModule (L : Type v) (M : Type w) [LieRing L] [AddCommGroup M] exten
 /-- A Lie module is a module over a commutative ring, together with a linear action of a Lie
 algebra on this module, such that the Lie bracket acts as the commutator of endomorphisms. -/
 class LieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L]
-  [AddCommGroup M] [Module R M] [LieRingModule L M] where
+  [AddCommGroup M] [Module R M] [LieRingModule L M] : Prop where
   /-- A Lie module bracket is compatible with scalar multiplication in its first argument. -/
   protected smul_lie : ∀ (t : R) (x : L) (m : M), ⁅t • x, m⁆ = t • ⁅x, m⁆
   /-- A Lie module bracket is compatible with scalar multiplication in its second argument. -/
@@ -467,9 +467,7 @@ variable (f : L₁ →ₗ⁅R⁆ L₂)
 /-- A Lie ring module may be pulled back along a morphism of Lie algebras.
 
 See note [reducible non-instances]. -/
-@[reducible]
-def LieRingModule.compLieHom : LieRingModule L₁ M
-    where
+def LieRingModule.compLieHom : LieRingModule L₁ M where
   bracket x m := ⁅f x, m⁆
   lie_add x := lie_add (f x)
   add_lie x y m := by simp only [LieHom.map_add, add_lie]
@@ -482,11 +480,8 @@ theorem LieRingModule.compLieHom_apply (x : L₁) (m : M) :
   rfl
 #align lie_ring_module.comp_lie_hom_apply LieRingModule.compLieHom_apply
 
-/-- A Lie module may be pulled back along a morphism of Lie algebras.
-
-See note [reducible non-instances]. -/
-@[reducible]
-def LieModule.compLieHom [Module R M] [LieModule R L₂ M] :
+/-- A Lie module may be pulled back along a morphism of Lie algebras. -/
+theorem LieModule.compLieHom [Module R M] [LieModule R L₂ M] :
     @LieModule R L₁ M _ _ _ _ _ (LieRingModule.compLieHom M f) :=
   { LieRingModule.compLieHom M f with
     smul_lie := fun t x m => by
diff --git a/Mathlib/Algebra/Lie/OfAssociative.lean b/Mathlib/Algebra/Lie/OfAssociative.lean
@@ -137,7 +137,7 @@ Lie algebra via the ring commutator.
 
 See the comment at `LieRingModule.ofAssociativeModule` for why the possibility `M = A` means
 this cannot be a global instance. -/
-def LieModule.ofAssociativeModule : LieModule R A M where
+theorem LieModule.ofAssociativeModule : LieModule R A M where
   smul_lie := smul_assoc
   lie_smul := smul_algebra_smul_comm
 #align lie_module.of_associative_module LieModule.ofAssociativeModule
diff --git a/Mathlib/Algebra/Order/ZeroLEOne.lean b/Mathlib/Algebra/Order/ZeroLEOne.lean
@@ -17,7 +17,7 @@ variable {α : Type _}
 open Function
 
 /-- Typeclass for expressing that the `0` of a type is less or equal to its `1`. -/
-class ZeroLEOneClass (α : Type _) [Zero α] [One α] [LE α] where
+class ZeroLEOneClass (α : Type _) [Zero α] [One α] [LE α] : Prop where
   /-- Zero is less than or equal to one. -/
   zero_le_one : (0 : α) ≤ 1
 #align zero_le_one_class ZeroLEOneClass
diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean
@@ -53,13 +53,13 @@ class Distrib (R : Type _) extends Mul R, Add R where
 #align distrib Distrib
 
 /-- A typeclass stating that multiplication is left distributive over addition. -/
-class LeftDistribClass (R : Type _) [Mul R] [Add R] where
+class LeftDistribClass (R : Type _) [Mul R] [Add R] : Prop where
   /-- Multiplication is left distributive over addition -/
   protected left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
 #align left_distrib_class LeftDistribClass
 
 /-- A typeclass stating that multiplication is right distributive over addition. -/
-class RightDistribClass (R : Type _) [Mul R] [Add R] where
+class RightDistribClass (R : Type _) [Mul R] [Add R] : Prop where
   /-- Multiplication is right distributive over addition -/
   protected right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c
 #align right_distrib_class RightDistribClass
diff --git a/Mathlib/Algebra/Star/CHSH.lean b/Mathlib/Algebra/Star/CHSH.lean
@@ -82,7 +82,7 @@ The physical interpretation is that `A₀` and `A₁` are a pair of boolean obse
 are spacelike separated from another pair `B₀` and `B₁` of boolean observables.
 -/
 --@[nolint has_nonempty_instance] Porting note: linter does not exist
-structure IsCHSHTuple {R} [Monoid R] [StarSemigroup R] (A₀ A₁ B₀ B₁ : R) where
+structure IsCHSHTuple {R} [Monoid R] [StarSemigroup R] (A₀ A₁ B₀ B₁ : R) : Prop where
   A₀_inv : A₀ ^ 2 = 1
   A₁_inv : A₁ ^ 2 = 1
   B₀_inv : B₀ ^ 2 = 1
diff --git a/Mathlib/Analysis/VonNeumannAlgebra/Basic.lean b/Mathlib/Analysis/VonNeumannAlgebra/Basic.lean
@@ -44,7 +44,7 @@ One the other hand, not picking one means that the weak-* topology
 and we may be unhappy with the resulting opaqueness of the definition.
 -/
 class WStarAlgebra (M : Type u) [NormedRing M] [StarRing M] [CstarRing M] [Module ℂ M]
-    [NormedAlgebra ℂ M] [StarModule ℂ M] where
+    [NormedAlgebra ℂ M] [StarModule ℂ M] : Prop where
   /-- There is a Banach space `X` whose dual is isometrically (conjugate-linearly) isomorphic
   to the `WStarAlgebra`. -/
   exists_predual :
diff --git a/Mathlib/CategoryTheory/Closed/Functor.lean b/Mathlib/CategoryTheory/Closed/Functor.lean
@@ -123,7 +123,7 @@ theorem expComparison_whiskerLeft {A A' : C} (f : A' ⟶ A) :
 /-- The functor `F` is cartesian closed (ie preserves exponentials) if each natural transformation
 `exp_comparison F A` is an isomorphism
 -/
-class CartesianClosedFunctor where
+class CartesianClosedFunctor : Prop where
   comparison_iso : ∀ A, IsIso (expComparison F A)
 #align category_theory.cartesian_closed_functor CategoryTheory.CartesianClosedFunctor
 
@@ -178,7 +178,7 @@ cartesian closed.
 TODO: Show the converse, that if `F` is cartesian closed and its left adjoint preserves binary
 products, then it is full and faithful.
 -/
-def cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts (h : L ⊣ F) [Full F] [Faithful F]
+theorem cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts (h : L ⊣ F) [Full F] [Faithful F]
     [PreservesLimitsOfShape (Discrete WalkingPair) L] : CartesianClosedFunctor F where
   comparison_iso _ := expComparison_iso_of_frobeniusMorphism_iso F h _
 #align category_theory.cartesian_closed_functor_of_left_adjoint_preserves_binary_products CategoryTheory.cartesianClosedFunctorOfLeftAdjointPreservesBinaryProducts
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean b/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean
@@ -142,7 +142,7 @@ Once we've set up `MonCat` as the category of bundled monoids,
 this allows us to set up `CommMonCat` by defining an instance
 ```instance : ParentProjection (CommMonoid.toMonoid) := ⟨⟩```
 -/
-class ParentProjection (F : ∀ {α}, d α → c α)
+class ParentProjection (F : ∀ {α}, d α → c α) : Prop
 #align category_theory.bundled_hom.parent_projection CategoryTheory.BundledHom.ParentProjection
 
 end
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/UnbundledHom.lean b/Mathlib/CategoryTheory/ConcreteCategory/UnbundledHom.lean
@@ -24,7 +24,7 @@ namespace CategoryTheory
 /-- A class for unbundled homs used to define a category. `hom` must
 take two types `α`, `β` and instances of the corresponding structures,
 and return a predicate on `α → β`. -/
-class UnbundledHom {c : Type u → Type u} (hom : ∀ ⦃α β⦄, c α → c β → (α → β) → Prop) where
+class UnbundledHom {c : Type u → Type u} (hom : ∀ ⦃α β⦄, c α → c β → (α → β) → Prop) : Prop where
   hom_id : ∀ {α} (ia : c α), hom ia ia id
   hom_comp : ∀ {α β γ} {Iα : c α} {Iβ : c β} {Iγ : c γ} {g : β → γ} {f : α → β} (_ : hom Iβ Iγ g)
       (_ : hom Iα Iβ f), hom Iα Iγ (g ∘ f)
diff --git a/Mathlib/CategoryTheory/EpiMono.lean b/Mathlib/CategoryTheory/EpiMono.lean
@@ -218,14 +218,14 @@ section
 variable (C)
 
 /-- A split mono category is a category in which every monomorphism is split. -/
-class SplitMonoCategory where
+class SplitMonoCategory : Prop where
   /-- All monos are split -/
   isSplitMono_of_mono : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], IsSplitMono f
 #align category_theory.split_mono_category CategoryTheory.SplitMonoCategory
 #align category_theory.split_mono_category.is_split_mono_of_mono CategoryTheory.SplitMonoCategory.isSplitMono_of_mono
 
 /-- A split epi category is a category in which every epimorphism is split. -/
-class SplitEpiCategory where
+class SplitEpiCategory : Prop where
   /-- All epis are split -/
   isSplitEpi_of_epi : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], IsSplitEpi f
 #align category_theory.split_epi_category CategoryTheory.SplitEpiCategory
diff --git a/Mathlib/CategoryTheory/Functor/EpiMono.lean b/Mathlib/CategoryTheory/Functor/EpiMono.lean
@@ -292,7 +292,7 @@ theorem mono_map_iff_mono [hF₁ : PreservesMonomorphisms F] [hF₂ : ReflectsMo
 
 /-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `split_epi_category`,
 then `D` also is. -/
-def splitEpiCategoryImpOfIsEquivalence [IsEquivalence F] [SplitEpiCategory C] :
+theorem splitEpiCategoryImpOfIsEquivalence [IsEquivalence F] [SplitEpiCategory C] :
     SplitEpiCategory D :=
   ⟨fun {X} {Y} f => by
     intro
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
@@ -849,7 +849,7 @@ section
 variable (C) [Category.{v} C] [HasImages C]
 
 /-- If a category `has_image_maps`, then all commutative squares induce morphisms on images. -/
-class HasImageMaps where
+class HasImageMaps : Prop where
   has_image_map : ∀ {f g : Arrow C} (st : f ⟶ g), HasImageMap st
 #align category_theory.limits.has_image_maps CategoryTheory.Limits.HasImageMaps
 
diff --git a/Mathlib/CategoryTheory/Monad/Monadicity.lean b/Mathlib/CategoryTheory/Monad/Monadicity.lean
@@ -276,7 +276,7 @@ local notation3 "adj" => Adjunction.ofRightAdjoint G
 -- Porting note: added these to replace parametric instances lean4#2311
 -- When this is fixed the proofs below that struggle with instances should be reviewed.
 -- [∀ ⦃A B⦄ (f g : A ⟶ B) [G.IsSplitPair f g], HasCoequalizer f g]
-class HasCoequalizerOfIsSplitPair (G : D ⥤ C) where
+class HasCoequalizerOfIsSplitPair (G : D ⥤ C) : Prop where
   out : ∀ {A B} (f g : A ⟶ B) [G.IsSplitPair f g], HasCoequalizer f g
 
 -- Porting note: cannot find synth order
diff --git a/Mathlib/CategoryTheory/Noetherian.lean b/Mathlib/CategoryTheory/Noetherian.lean
@@ -60,14 +60,14 @@ lemma ArtinianObject.subobject_lt_wellFounded (X : C) [ArtinianObject X] :
 variable (C)
 
 /-- A category is noetherian if it is essentially small and all objects are noetherian. -/
-class Noetherian extends EssentiallySmall C where
+class Noetherian extends EssentiallySmall C : Prop where
   noetherianObject : ∀ X : C, NoetherianObject X
 #align category_theory.noetherian CategoryTheory.Noetherian
 
 attribute [instance] Noetherian.noetherianObject
 
 /-- A category is artinian if it is essentially small and all objects are artinian. -/
-class Artinian extends EssentiallySmall C where
+class Artinian extends EssentiallySmall C : Prop where
   artinianObject : ∀ X : C, ArtinianObject X
 #align category_theory.artinian CategoryTheory.Artinian
 
diff --git a/Mathlib/CategoryTheory/Triangulated/Triangulated.lean b/Mathlib/CategoryTheory/Triangulated/Triangulated.lean
@@ -119,7 +119,7 @@ open Triangulated
 
 /-- A triangulated category is a pretriangulated category which satisfies
 the octahedron axiom (TR 4), see https://stacks.math.columbia.edu/tag/05QK -/
-class IsTriangulated where
+class IsTriangulated : Prop where
   /-- the octahedron axiom (TR 4) -/
   octahedron_axiom :
     ∀ {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C}
diff --git a/Mathlib/Combinatorics/Quiver/Symmetric.lean b/Mathlib/Combinatorics/Quiver/Symmetric.lean
@@ -83,7 +83,7 @@ section MapReverse
 variable [HasReverse U] [HasReverse V] [HasReverse W]
 
 /-- A prefunctor preserving reversal of arrows -/
-class _root_.Prefunctor.MapReverse (φ : U ⥤q V) where
+class _root_.Prefunctor.MapReverse (φ : U ⥤q V) : Prop where
   /-- The image of a reverse is the reverse of the image. -/
   map_reverse' : ∀ {u v : U} (e : u ⟶ v), φ.map (reverse e) = reverse (φ.map e)
 #align prefunctor.map_reverse Prefunctor.MapReverse
diff --git a/Mathlib/Control/Bifunctor.lean b/Mathlib/Control/Bifunctor.lean
@@ -38,7 +38,7 @@ class Bifunctor (F : Type u₀ → Type u₁ → Type u₂) where
 export Bifunctor (bimap)
 
 /-- Bifunctor. This typeclass asserts that a lawless `Bifunctor` is lawful. -/
-class LawfulBifunctor (F : Type u₀ → Type u₁ → Type u₂) [Bifunctor F] where
+class LawfulBifunctor (F : Type u₀ → Type u₁ → Type u₂) [Bifunctor F] : Prop where
   id_bimap : ∀ {α β} (x : F α β), bimap id id x = x
   bimap_bimap :
     ∀ {α₀ α₁ α₂ β₀ β₁ β₂} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂) (x : F α₀ β₀),
diff --git a/Mathlib/Control/Bitraversable/Basic.lean b/Mathlib/Control/Bitraversable/Basic.lean
@@ -60,7 +60,7 @@ open Functor
 
 /-- Bifunctor. This typeclass asserts that a lawless bitraversable bifunctor is lawful. -/
 class LawfulBitraversable (t : Type u → Type u → Type u) [Bitraversable t] extends
-  LawfulBifunctor t where
+  LawfulBifunctor t : Prop where
   -- Porting note: need to specify `m := Id` because `id` no longer has a `Monad` instance
   id_bitraverse : ∀ {α β} (x : t α β), bitraverse (m := Id) pure pure x = pure x
   comp_bitraverse :
diff --git a/Mathlib/Control/Monad/Cont.lean b/Mathlib/Control/Monad/Cont.lean
@@ -33,7 +33,8 @@ class MonadCont (m : Type u → Type v) where
 
 open MonadCont
 
-class LawfulMonadCont (m : Type u → Type v) [Monad m] [MonadCont m] extends LawfulMonad m where
+class LawfulMonadCont (m : Type u → Type v) [Monad m] [MonadCont m]
+    extends LawfulMonad m : Prop where
   callCC_bind_right {α ω γ} (cmd : m α) (next : Label ω m γ → α → m ω) :
     (callCC fun f => cmd >>= next f) = cmd >>= fun x => callCC fun f => next f x
   callCC_bind_left {α} (β) (x : α) (dead : Label α m β → β → m α) :
diff --git a/Mathlib/Control/Traversable/Basic.lean b/Mathlib/Control/Traversable/Basic.lean
@@ -248,7 +248,7 @@ send the composition of applicative functors to the composition of the
 satisfy a naturality condition with respect to applicative
 transformations. -/
 class LawfulTraversable (t : Type u → Type u) [Traversable t] extends LawfulFunctor t :
-    Type (u + 1) where
+    Prop where
   /-- `traverse` plays well with `pure` of the identity monad-/
   id_traverse : ∀ {α} (x : t α), traverse (pure : α → Id α) x = x
   /-- `traverse` plays well with composition of applicative functors. -/
diff --git a/Mathlib/Control/Traversable/Equiv.lean b/Mathlib/Control/Traversable/Equiv.lean
@@ -154,7 +154,7 @@ protected theorem naturality (f : α → F β) (x : t' α) :
 /-- The fact that `t` is a lawful traversable functor carries over the
 equivalences to `t'`, with the traversable functor structure given by
 `Equiv.traversable`. -/
-protected def isLawfulTraversable : @LawfulTraversable t' (Equiv.traversable eqv) :=
+protected theorem isLawfulTraversable : @LawfulTraversable t' (Equiv.traversable eqv) :=
   -- Porting note: Same `_inst` local variable problem.
   let _inst := Equiv.traversable eqv; {
     toLawfulFunctor := Equiv.lawfulFunctor eqv
@@ -169,7 +169,7 @@ protected def isLawfulTraversable : @LawfulTraversable t' (Equiv.traversable eqv
 carrying the traversable functor structure from `t` over the
 equivalences, then the fact that `t` is a lawful traversable functor
 carries over as well. -/
-protected def isLawfulTraversable' [Traversable t']
+protected theorem isLawfulTraversable' [Traversable t']
     (h₀ : ∀ {α β} (f : α → β), map f = Equiv.map eqv f)
     (h₁ : ∀ {α β} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f)
     (h₂ :
diff --git a/Mathlib/Data/Fin/Fin2.lean b/Mathlib/Data/Fin/Fin2.lean
@@ -107,7 +107,7 @@ def remapLeft {m n} (f : Fin2 m → Fin2 n) : ∀ k, Fin2 (m + k) → Fin2 (n +
 
 /-- This is a simple type class inference prover for proof obligations
   of the form `m < n` where `m n : ℕ`. -/
-class IsLT (m n : ℕ) where
+class IsLT (m n : ℕ) : Prop where
   /-- The unique field of `Fin2.IsLT`, a proof that `m < n`. -/
   h : m < n
 #align fin2.is_lt Fin2.IsLT
@@ -121,9 +121,9 @@ instance IsLT.succ (m n) [l : IsLT m n] : IsLT (succ m) (succ n) :=
 /-- Use type class inference to infer the boundedness proof, so that we can directly convert a
 `Nat` into a `Fin2 n`. This supports notation like `&1 : Fin 3`. -/
 def ofNat' : ∀ {n} (m) [IsLT m n], Fin2 n
-  | 0, _, ⟨h⟩ => absurd h (Nat.not_lt_zero _)
-  | succ _, 0, ⟨_⟩ => fz
-  | succ n, succ m, ⟨h⟩ => fs (@ofNat' n m ⟨lt_of_succ_lt_succ h⟩)
+  | 0, _, h => absurd h.h (Nat.not_lt_zero _)
+  | succ _, 0, _ => fz
+  | succ n, succ m, h => fs (@ofNat' n m ⟨lt_of_succ_lt_succ h.h⟩)
 #align fin2.of_nat' Fin2.ofNat'
 
 @[inherit_doc] local prefix:arg "&" => ofNat'
diff --git a/Mathlib/GroupTheory/GroupAction/SubMulAction.lean b/Mathlib/GroupTheory/GroupAction/SubMulAction.lean
@@ -44,7 +44,8 @@ scalar action of `R` on `M`.
 Note that only `R` is marked as an `outParam` here, since `M` is supplied by the `SetLike`
 class instead.
 -/
-class SMulMemClass (S : Type _) (R : outParam <| Type _) (M : Type _) [SMul R M] [SetLike S M] where
+class SMulMemClass (S : Type _) (R : outParam <| Type _) (M : Type _) [SMul R M] [SetLike S M] :
+    Prop where
   /-- Multiplication by a scalar on an element of the set remains in the set. -/
   smul_mem : ∀ {s : S} (r : R) {m : M}, m ∈ s → r • m ∈ s
 #align smul_mem_class SMulMemClass
@@ -54,7 +55,8 @@ additive action of `R` on `M`.
 
 Note that only `R` is marked as an `outParam` here, since `M` is supplied by the `SetLike`
 class instead. -/
-class VAddMemClass (S : Type _) (R : outParam <| Type _) (M : Type _) [VAdd R M] [SetLike S M] where
+class VAddMemClass (S : Type _) (R : outParam <| Type _) (M : Type _) [VAdd R M] [SetLike S M] :
+    Prop where
   /-- Addition by a scalar with an element of the set remains in the set. -/
   vadd_mem : ∀ {s : S} (r : R) {m : M}, m ∈ s → r +ᵥ m ∈ s
 #align vadd_mem_class VAddMemClass
@@ -77,7 +79,7 @@ instance (priority := 900) smul : SMul R s :=
 
 /-- This can't be an instance because Lean wouldn't know how to find `N`, but we can still use
 this to manually derive `SMulMemClass` on specific types. -/
-def _root_.SMulMemClass.ofIsScalarTower (S M N α : Type _) [SetLike S α] [SMul M N]
+theorem _root_.SMulMemClass.ofIsScalarTower (S M N α : Type _) [SetLike S α] [SMul M N]
   [SMul M α] [Monoid N] [MulAction N α] [SMulMemClass S N α] [IsScalarTower M N α] :
   SMulMemClass S M α :=
 { smul_mem := fun m a ha => smul_one_smul N m a ▸ SMulMemClass.smul_mem _ ha }
diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean
@@ -167,7 +167,7 @@ Note that `Module R' (M ⊗[R] N)` is available even without this typeclass on `
 needed if `TensorProduct.smul_tmul`, `TensorProduct.smul_tmul'`, or `TensorProduct.tmul_smul` is
 used.
 -/
-class CompatibleSMul [DistribMulAction R' N] where
+class CompatibleSMul [DistribMulAction R' N] : Prop where
   smul_tmul : ∀ (r : R') (m : M) (n : N), (r • m) ⊗ₜ n = m ⊗ₜ[R] (r • n)
 #align tensor_product.compatible_smul TensorProduct.CompatibleSMul
 
diff --git a/Mathlib/MeasureTheory/Group/Arithmetic.lean b/Mathlib/MeasureTheory/Group/Arithmetic.lean
@@ -192,7 +192,7 @@ theorem measurable_div_const' {G : Type _} [DivInvMonoid G] [MeasurableSpace G]
 #align measurable_sub_const' measurable_sub_const'
 
 /-- This class assumes that the map `β × γ → β` given by `(x, y) ↦ x ^ y` is measurable. -/
-class MeasurablePow (β γ : Type _) [MeasurableSpace β] [MeasurableSpace γ] [Pow β γ] where
+class MeasurablePow (β γ : Type _) [MeasurableSpace β] [MeasurableSpace γ] [Pow β γ] : Prop where
   measurable_pow : Measurable fun p : β × γ => p.1 ^ p.2
 #align has_measurable_pow MeasurablePow
 
diff --git a/Mathlib/MeasureTheory/Measure/Doubling.lean b/Mathlib/MeasureTheory/Measure/Doubling.lean
@@ -42,7 +42,7 @@ volumes grow exponentially in hyperbolic space. To be really explicit, consider
 of curvature -1, the area of a disc of radius `ε` is `A(ε) = 2π(cosh(ε) - 1)` so
 `A(2ε)/A(ε) ~ exp(ε)`. -/
 class IsUnifLocDoublingMeasure {α : Type _} [MetricSpace α] [MeasurableSpace α]
-  (μ : Measure α) where
+  (μ : Measure α) : Prop where
   exists_measure_closedBall_le_mul'' :
     ∃ C : ℝ≥0, ∀ᶠ ε in 𝓝[>] 0, ∀ x, μ (closedBall x (2 * ε)) ≤ C * μ (closedBall x ε)
 #align is_unif_loc_doubling_measure IsUnifLocDoublingMeasure
diff --git a/Mathlib/ModelTheory/Basic.lean b/Mathlib/ModelTheory/Basic.lean
diff --git a/Mathlib/Order/RelClasses.lean b/Mathlib/Order/RelClasses.lean
diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean
diff --git a/Mathlib/Tactic/Lift.lean b/Mathlib/Tactic/Lift.lean
diff --git a/Mathlib/Tactic/Lint.lean b/Mathlib/Tactic/Lint.lean
diff --git a/Mathlib/Topology/Order/Lattice.lean b/Mathlib/Topology/Order/Lattice.lean
diff --git a/Mathlib/Topology/Order/Priestley.lean b/Mathlib/Topology/Order/Priestley.lean
