From 986c4d5761f938b2e1c43c01f001b6d9d88c2055 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Thu, 29 Dec 2022 17:01:52 +0000
Subject: [PATCH] fix(*): mark some classes as Prop (#18015)

---
 .../100-theorems-list/30_ballot_problem.lean   |  2 +-
 src/algebra/hom/freiman.lean                   |  6 +++---
 .../projective_spectrum/scheme.lean            |  8 ++++----
 src/category_theory/monoidal/linear.lean       |  4 ++--
 src/category_theory/monoidal/preadditive.lean  |  4 ++--
 src/field_theory/subfield.lean                 |  2 +-
 src/group_theory/subgroup/basic.lean           | 18 +++++-------------
 src/group_theory/submonoid/basic.lean          | 15 ++++-----------
 src/group_theory/subsemigroup/basic.lean       |  4 ++--
 src/ring_theory/subring/basic.lean             |  3 +--
 src/ring_theory/subsemiring/basic.lean         |  6 ++----
 11 files changed, 27 insertions(+), 45 deletions(-)

diff --git a/archive/100-theorems-list/30_ballot_problem.lean b/archive/100-theorems-list/30_ballot_problem.lean
index 4891ab851160e..6e9e589531cce 100644
--- a/archive/100-theorems-list/30_ballot_problem.lean
+++ b/archive/100-theorems-list/30_ballot_problem.lean
@@ -277,7 +277,7 @@ private def measureable_space_list_int : measurable_space (list ℤ) := ⊤
 
 local attribute [instance] measureable_space_list_int
 
-private def measurable_singleton_class_list_int : measurable_singleton_class (list ℤ) :=
+private lemma measurable_singleton_class_list_int : measurable_singleton_class (list ℤ) :=
 { measurable_set_singleton := λ s, trivial }
 
 local attribute [instance] measurable_singleton_class_list_int
diff --git a/src/algebra/hom/freiman.lean b/src/algebra/hom/freiman.lean
index 3f880ffd34a70..f55b01bfd49b5 100644
--- a/src/algebra/hom/freiman.lean
+++ b/src/algebra/hom/freiman.lean
@@ -72,7 +72,7 @@ notation (name := freiman_hom) A ` →*[`:25 n:25 `] `:0 β:0 := freiman_hom A 
 /-- `add_freiman_hom_class F s β n` states that `F` is a type of `n`-ary sums-preserving morphisms.
 You should extend this class when you extend `add_freiman_hom`. -/
 class add_freiman_hom_class (F : Type*) (A : out_param $ set α) (β : out_param $ Type*)
-  [add_comm_monoid α] [add_comm_monoid β] (n : ℕ) [fun_like F α (λ _, β)] :=
+  [add_comm_monoid α] [add_comm_monoid β] (n : ℕ) [fun_like F α (λ _, β)] : Prop :=
 (map_sum_eq_map_sum' (f : F) {s t : multiset α} (hsA : ∀ ⦃x⦄, x ∈ s → x ∈ A)
   (htA : ∀ ⦃x⦄, x ∈ t → x ∈ A) (hs : s.card = n) (ht : t.card = n) (h : s.sum = t.sum) :
   (s.map f).sum = (t.map f).sum)
@@ -83,7 +83,7 @@ You should extend this class when you extend `freiman_hom`. -/
 "`add_freiman_hom_class F A β n` states that `F` is a type of `n`-ary sums-preserving morphisms.
 You should extend this class when you extend `add_freiman_hom`."]
 class freiman_hom_class (F : Type*) (A : out_param $ set α) (β : out_param $ Type*) [comm_monoid α]
-  [comm_monoid β] (n : ℕ) [fun_like F α (λ _, β)] :=
+  [comm_monoid β] (n : ℕ) [fun_like F α (λ _, β)] : Prop :=
 (map_prod_eq_map_prod' (f : F) {s t : multiset α} (hsA : ∀ ⦃x⦄, x ∈ s → x ∈ A)
   (htA : ∀ ⦃x⦄, x ∈ t → x ∈ A) (hs : s.card = n) (ht : t.card = n) (h : s.prod = t.prod) :
   (s.map f).prod = (t.map f).prod)
@@ -369,7 +369,7 @@ def freiman_hom.to_freiman_hom (h : m ≤ n) (f : A →*[n] β) : A →*[m] β :
 /-- A `n`-Freiman homomorphism is also a `m`-Freiman homomorphism for any `m ≤ n`. -/
 @[to_additive add_freiman_hom.add_freiman_hom_class_of_le "An additive `n`-Freiman homomorphism is
 also an additive `m`-Freiman homomorphism for any `m ≤ n`."]
-def freiman_hom.freiman_hom_class_of_le [freiman_hom_class F A β n] (h : m ≤ n) :
+lemma freiman_hom.freiman_hom_class_of_le [freiman_hom_class F A β n] (h : m ≤ n) :
   freiman_hom_class F A β m :=
 { map_prod_eq_map_prod' := λ f s t hsA htA hs ht hst,
     map_prod_eq_map_prod_of_le f hsA htA hs ht hst h }
diff --git a/src/algebraic_geometry/projective_spectrum/scheme.lean b/src/algebraic_geometry/projective_spectrum/scheme.lean
index 1ae0d6c22164a..3d28c47c871a3 100644
--- a/src/algebraic_geometry/projective_spectrum/scheme.lean
+++ b/src/algebraic_geometry/projective_spectrum/scheme.lean
@@ -196,8 +196,8 @@ begin
   rw set.not_disjoint_iff_nonempty_inter,
   refine ⟨f^N * f^M, eq1.symm ▸ mul_mem_right _ _
     (sum_mem _ (λ i hi, mul_mem_left _ _ _)), ⟨N+M, by rw pow_add⟩⟩,
-  generalize_proofs h,
-  exact (classical.some_spec h).1,
+  generalize_proofs h₁ h₂,
+  exact (classical.some_spec h₂).1,
 end
 
 variable (f)
@@ -236,7 +236,7 @@ def to_fun (x : Proj.T| (pbo f)) : (Spec.T (A⁰_ f)) :=
   { exact false.elim (x.2 (x.1.is_prime.mem_of_pow_mem M rid2)), },
   { rw [mul_comm _ (f^N), eq1],
     refine mul_mem_right _ _ (mul_mem_right _ _ (sum_mem _ (λ i hi, mul_mem_left _ _ _))),
-    generalize_proofs h, exact (classical.some_spec h).1 },
+    generalize_proofs h₁ h₂, exact (classical.some_spec h₂).1 },
 end⟩
 
 /-
@@ -283,7 +283,7 @@ begin
     { exact y.2 (y.1.is_prime.mem_of_pow_mem M H3), },
     { rw [mul_comm _ (f^N), eq1],
       refine mul_mem_right _ _ (mul_mem_right _ _ (sum_mem _ (λ i hi, mul_mem_left _ _ _))),
-      generalize_proofs h, exact (classical.some_spec h).1, }, },
+      generalize_proofs h₁ h₂, exact (classical.some_spec h₂).1, }, },
 end
 
 end to_Spec
diff --git a/src/category_theory/monoidal/linear.lean b/src/category_theory/monoidal/linear.lean
index 75d95bead92ff..adf3555e1fcec 100644
--- a/src/category_theory/monoidal/linear.lean
+++ b/src/category_theory/monoidal/linear.lean
@@ -25,7 +25,7 @@ variables [monoidal_category C] [monoidal_preadditive C]
 /--
 A category is `monoidal_linear R` if tensoring is `R`-linear in both factors.
 -/
-class monoidal_linear :=
+class monoidal_linear : Prop :=
 (tensor_smul' : ∀ {W X Y Z : C} (f : W ⟶ X) (r : R) (g : Y ⟶ Z),
   f ⊗ (r • g) = r • (f ⊗ g) . obviously)
 (smul_tensor' : ∀ {W X Y Z : C} (r : R) (f : W ⟶ X) (g : Y ⟶ Z),
@@ -44,7 +44,7 @@ instance tensoring_right_linear (X : C) : ((tensoring_right C).obj X).linear R :
 
 /-- A faithful linear monoidal functor to a linear monoidal category
 ensures that the domain is linear monoidal. -/
-def monoidal_linear_of_faithful
+lemma monoidal_linear_of_faithful
   {D : Type*} [category D] [preadditive D] [linear R D]
   [monoidal_category D] [monoidal_preadditive D]
   (F : monoidal_functor D C) [faithful F.to_functor]
diff --git a/src/category_theory/monoidal/preadditive.lean b/src/category_theory/monoidal/preadditive.lean
index 10c0e82a49605..9fb5c2b68234f 100644
--- a/src/category_theory/monoidal/preadditive.lean
+++ b/src/category_theory/monoidal/preadditive.lean
@@ -29,7 +29,7 @@ A category is `monoidal_preadditive` if tensoring is additive in both factors.
 Note we don't `extend preadditive C` here, as `abelian C` already extends it,
 and we'll need to have both typeclasses sometimes.
 -/
-class monoidal_preadditive :=
+class monoidal_preadditive : Prop :=
 (tensor_zero' : ∀ {W X Y Z : C} (f : W ⟶ X), f ⊗ (0 : Y ⟶ Z) = 0 . obviously)
 (zero_tensor' : ∀ {W X Y Z : C} (f : Y ⟶ Z), (0 : W ⟶ X) ⊗ f = 0 . obviously)
 (tensor_add' : ∀ {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h . obviously)
@@ -52,7 +52,7 @@ instance tensoring_right_additive (X : C) : ((tensoring_right C).obj X).additive
 
 /-- A faithful additive monoidal functor to a monoidal preadditive category
 ensures that the domain is monoidal preadditive. -/
-def monoidal_preadditive_of_faithful {D : Type*} [category D] [preadditive D] [monoidal_category D]
+lemma monoidal_preadditive_of_faithful {D} [category D] [preadditive D] [monoidal_category D]
   (F : monoidal_functor D C) [faithful F.to_functor] [F.to_functor.additive] :
   monoidal_preadditive D :=
 { tensor_zero' := by { intros, apply F.to_functor.map_injective, simp [F.map_tensor], },
diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean
index d704fc08fbd46..1f66d94ff24e0 100644
--- a/src/field_theory/subfield.lean
+++ b/src/field_theory/subfield.lean
@@ -66,7 +66,7 @@ variables {K : Type u} {L : Type v} {M : Type w} [field K] [field L] [field M]
 
 /-- `subfield_class S K` states `S` is a type of subsets `s ⊆ K` closed under field operations. -/
 class subfield_class (S : Type*) (K : out_param $ Type*) [field K] [set_like S K]
-  extends subring_class S K, inv_mem_class S K.
+  extends subring_class S K, inv_mem_class S K : Prop
 
 namespace subfield_class
 
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
index 2afc191ebafc8..2cf2efd18c74e 100644
--- a/src/group_theory/subgroup/basic.lean
+++ b/src/group_theory/subgroup/basic.lean
@@ -95,39 +95,31 @@ variables {A : Type*} [add_group A]
 section subgroup_class
 
 /-- `inv_mem_class S G` states `S` is a type of subsets `s ⊆ G` closed under inverses. -/
-class inv_mem_class (S G : Type*) [has_inv G] [set_like S G] :=
+class inv_mem_class (S G : Type*) [has_inv G] [set_like S G] : Prop :=
 (inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s)
 
 export inv_mem_class (inv_mem)
 
 /-- `neg_mem_class S G` states `S` is a type of subsets `s ⊆ G` closed under negation. -/
-class neg_mem_class (S G : Type*) [has_neg G] [set_like S G] :=
+class neg_mem_class (S G : Type*) [has_neg G] [set_like S G] : Prop :=
 (neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s)
 
 export neg_mem_class (neg_mem)
 
 /-- `subgroup_class S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`. -/
 class subgroup_class (S G : Type*) [div_inv_monoid G] [set_like S G]
-  extends submonoid_class S G :=
-(inv_mem : ∀ {s : S} {x}, x ∈ s → x⁻¹ ∈ s)
+  extends submonoid_class S G, inv_mem_class S G : Prop
 
 /-- `add_subgroup_class S G` states `S` is a type of subsets `s ⊆ G` that are
 additive subgroups of `G`. -/
 class add_subgroup_class (S G : Type*) [sub_neg_monoid G] [set_like S G]
-  extends add_submonoid_class S G :=
-(neg_mem : ∀ {s : S} {x}, x ∈ s → -x ∈ s)
+  extends add_submonoid_class S G, neg_mem_class S G : Prop
 
 attribute [to_additive] inv_mem_class subgroup_class
 
-variables (M S : Type*) [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M]
+variables {M S : Type*} [div_inv_monoid M] [set_like S M] [hSM : subgroup_class S M] {H K : S}
 include hSM
 
-@[to_additive, priority 100] -- See note [lower instance priority]
-instance subgroup_class.to_inv_mem_class : inv_mem_class S M :=
-{ .. hSM }
-
-variables {S M} {H K : S}
-
 /-- A subgroup is closed under division. -/
 @[to_additive "An additive subgroup is closed under subtraction."]
 theorem div_mem {x y : M} (hx : x ∈ H) (hy : y ∈ H) : x / y ∈ H :=
diff --git a/src/group_theory/submonoid/basic.lean b/src/group_theory/submonoid/basic.lean
index afde4a523284c..8fa051273cbc5 100644
--- a/src/group_theory/submonoid/basic.lean
+++ b/src/group_theory/submonoid/basic.lean
@@ -60,13 +60,13 @@ variables [mul_one_class M] {s : set M}
 variables [add_zero_class A] {t : set A}
 
 /-- `one_mem_class S M` says `S` is a type of subsets `s ≤ M`, such that `1 ∈ s` for all `s`. -/
-class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] [set_like S M] :=
+class one_mem_class (S : Type*) (M : out_param $ Type*) [has_one M] [set_like S M] : Prop :=
 (one_mem : ∀ (s : S), (1 : M) ∈ s)
 
 export one_mem_class (one_mem)
 
 /-- `zero_mem_class S M` says `S` is a type of subsets `s ≤ M`, such that `0 ∈ s` for all `s`. -/
-class zero_mem_class (S : Type*) (M : out_param $ Type*) [has_zero M] [set_like S M] :=
+class zero_mem_class (S : Type*) (M : out_param $ Type*) [has_zero M] [set_like S M] : Prop :=
 (zero_mem : ∀ (s : S), (0 : M) ∈ s)
 
 export zero_mem_class (zero_mem)
@@ -90,8 +90,7 @@ add_decl_doc submonoid.to_subsemigroup
 /-- `submonoid_class S M` says `S` is a type of subsets `s ≤ M` that contain `1`
 and are closed under `(*)` -/
 class submonoid_class (S : Type*) (M : out_param $ Type*) [mul_one_class M] [set_like S M]
-  extends mul_mem_class S M :=
-(one_mem : ∀ (s : S), (1 : M) ∈ s)
+  extends mul_mem_class S M, one_mem_class S M : Prop
 
 section
 
@@ -112,16 +111,10 @@ add_decl_doc add_submonoid.to_add_subsemigroup
 /-- `add_submonoid_class S M` says `S` is a type of subsets `s ≤ M` that contain `0`
 and are closed under `(+)` -/
 class add_submonoid_class (S : Type*) (M : out_param $ Type*) [add_zero_class M] [set_like S M]
-  extends add_mem_class S M :=
-(zero_mem : ∀ (s : S), (0 : M) ∈ s)
+  extends add_mem_class S M, zero_mem_class S M : Prop
 
 attribute [to_additive] submonoid submonoid_class
 
-@[to_additive, priority 100] -- See note [lower instance priority]
-instance submonoid_class.to_one_mem_class (S : Type*) (M : out_param $ Type*) [mul_one_class M]
-  [set_like S M] [h : submonoid_class S M] : one_mem_class S M :=
-{ ..h }
-
 @[to_additive]
 lemma pow_mem {M} [monoid M] {A : Type*} [set_like A M] [submonoid_class A M] {S : A} {x : M}
   (hx : x ∈ S) : ∀ (n : ℕ), x ^ n ∈ S
diff --git a/src/group_theory/subsemigroup/basic.lean b/src/group_theory/subsemigroup/basic.lean
index 0c7c232cd6857..28d6e513792c9 100644
--- a/src/group_theory/subsemigroup/basic.lean
+++ b/src/group_theory/subsemigroup/basic.lean
@@ -54,13 +54,13 @@ variables [has_mul M] {s : set M}
 variables [has_add A] {t : set A}
 
 /-- `mul_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(*)` -/
-class mul_mem_class (S : Type*) (M : out_param $ Type*) [has_mul M] [set_like S M] :=
+class mul_mem_class (S : Type*) (M : out_param $ Type*) [has_mul M] [set_like S M] : Prop :=
 (mul_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a * b ∈ s)
 
 export mul_mem_class (mul_mem)
 
 /-- `add_mem_class S M` says `S` is a type of subsets `s ≤ M` that are closed under `(+)` -/
-class add_mem_class (S : Type*) (M : out_param $ Type*) [has_add M] [set_like S M] :=
+class add_mem_class (S : Type*) (M : out_param $ Type*) [has_add M] [set_like S M] : Prop :=
 (add_mem : ∀ {s : S} {a b : M}, a ∈ s → b ∈ s → a + b ∈ s)
 
 export add_mem_class (add_mem)
diff --git a/src/ring_theory/subring/basic.lean b/src/ring_theory/subring/basic.lean
index 44a1a9fb8c92f..54ea6c2f32073 100644
--- a/src/ring_theory/subring/basic.lean
+++ b/src/ring_theory/subring/basic.lean
@@ -72,8 +72,7 @@ section subring_class
 /-- `subring_class S R` states that `S` is a type of subsets `s ⊆ R` that
 are both a multiplicative submonoid and an additive subgroup. -/
 class subring_class (S : Type*) (R : out_param $ Type u) [ring R] [set_like S R]
-  extends subsemiring_class S R :=
-(neg_mem : ∀ {s : S} {a : R}, a ∈ s → -a ∈ s)
+  extends subsemiring_class S R, neg_mem_class S R : Prop
 
 @[priority 100] -- See note [lower instance priority]
 instance subring_class.add_subgroup_class (S : Type*) (R : out_param $ Type u) [set_like S R]
diff --git a/src/ring_theory/subsemiring/basic.lean b/src/ring_theory/subsemiring/basic.lean
index 3396929e837c8..f064254ef77bd 100644
--- a/src/ring_theory/subsemiring/basic.lean
+++ b/src/ring_theory/subsemiring/basic.lean
@@ -31,7 +31,7 @@ section add_submonoid_with_one_class
 and are closed under `(+)` -/
 class add_submonoid_with_one_class (S : Type*) (R : out_param $ Type*)
   [add_monoid_with_one R] [set_like S R]
-  extends add_submonoid_class S R, one_mem_class S R
+  extends add_submonoid_class S R, one_mem_class S R : Prop
 
 variables {S R : Type*} [add_monoid_with_one R] [set_like S R] (s : S)
 
@@ -56,9 +56,7 @@ section subsemiring_class
 /-- `subsemiring_class S R` states that `S` is a type of subsets `s ⊆ R` that
 are both a multiplicative and an additive submonoid. -/
 class subsemiring_class (S : Type*) (R : out_param $ Type u) [non_assoc_semiring R] [set_like S R]
-  extends submonoid_class S R :=
-(add_mem : ∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a + b ∈ s)
-(zero_mem : ∀ (s : S), (0 : R) ∈ s)
+  extends submonoid_class S R, add_submonoid_class S R : Prop
 
 @[priority 100] -- See note [lower instance priority]
 instance subsemiring_class.add_submonoid_with_one_class (S : Type*) (R : out_param $ Type u)