chore(CategoryTheory): reduce Set α = α → Prop defeq abuse (leanprover-community#36115)

Author: urkud

Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

@@ -522,7 +522,7 @@ variable (W') in
 and the set of pairs `⟨x, y⟩` satisfying `W.Nonsingular x y` with zero. -/
 def nonsingularPointEquiv : W'.Point ≃ WithZero {xy : R × R // W'.Nonsingular xy.fst xy.snd} :=
   (Equiv.Set.univ W'.Point).symm.trans <| (nonsingularPointEquivSubtype trivial).trans
-    (Equiv.setCongr <| Set.ext fun _ => exists_iff_of_forall fun _ => trivial).optionCongr
+    (Equiv.subtypeEquivProp <| by simp).optionCongr
 
 @[simp]
 lemma nonsingularPointEquiv_zero : nonsingularPointEquiv W' .zero = none :=
@@ -555,7 +555,7 @@ predicate and the set of pairs `⟨x, y⟩` satisfying `W.Equation x y` with zer
 def pointEquivSubtype {p : W'.Point → Prop} (p0 : p .zero) :
     {P : W'.Point // p P} ≃ WithZero {xy : R × R // ∃ h : W'.Equation xy.fst xy.snd, p <| .mk h} :=
   (nonsingularPointEquivSubtype p0).trans
-    (Equiv.setCongr <| by simp [equation_iff_nonsingular, Point.mk]).optionCongr
+    (Equiv.subtypeEquivProp <| by ext; simp [equation_iff_nonsingular, Point.mk]).optionCongr
 
 @[simp]
 lemma pointEquivSubtype_zero {p : W'.Point → Prop} (p0 : p .zero) :
@@ -583,7 +583,7 @@ variable (W') in
 `⟨x, y⟩` satisfying `E.Equation x y` with zero. -/
 def pointEquiv : W'.Point ≃ WithZero {xy : R × R // W'.Equation xy.fst xy.snd} :=
   (Equiv.Set.univ W'.Point).symm.trans <| (pointEquivSubtype trivial).trans
-    (Equiv.setCongr <| Set.ext fun _ => exists_iff_of_forall fun _ => trivial).optionCongr
+    (Equiv.subtypeEquivProp <| by simp).optionCongr
 
 @[simp]
 lemma pointEquiv_zero : W'.pointEquiv .zero = none :=

Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean

@@ -564,7 +564,7 @@ set_option backward.isDefEq.respectTransparency false in
 which is the largest ideal sheaf whose support is equal to it.
 The reduced induced scheme structure on the closed set is the quotient of this ideal. -/
 @[simps! ideal coe_support]
-nonrec def vanishingIdeal (Z : Closeds X) : IdealSheafData X :=
+noncomputable nonrec def vanishingIdeal (Z : Closeds X) : IdealSheafData X :=
   mkOfMemSupportIff
     (fun U ↦ vanishingIdeal (U.2.fromSpec ⁻¹' Z))
     (fun U f ↦ by

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -552,11 +552,11 @@ def fromSpec {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
   TopCat.ofHom
   { toFun := FromSpec.toFun f_deg hm
     continuous_toFun := by
-      rw [isTopologicalBasis_subtype (ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜) (pbo f).1
-        |>.continuous_iff]
+      rw [isTopologicalBasis_subtype (ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜)
+        (· ∈ pbo f) |>.continuous_iff]
       rintro s ⟨_, ⟨a, rfl⟩, rfl⟩
-      have h₁ : Subtype.val (p := (pbo f).1) ⁻¹' (pbo a) =
-          ⋃ i : ℕ, Subtype.val (p := (pbo f).1) ⁻¹' (pbo (decompose 𝒜 a i)) := by
+      have h₁ : Subtype.val (p := (· ∈ pbo f)) ⁻¹' (pbo a) =
+          ⋃ i : ℕ, Subtype.val (p := (· ∈ pbo f)) ⁻¹' (pbo (decompose 𝒜 a i)) := by
         simp [ProjectiveSpectrum.basicOpen_eq_union_of_projection 𝒜 a]
       let e : _ ≃ _ :=
         ⟨FromSpec.toFun f_deg hm, ToSpec.toFun f, toSpec_fromSpec _ _ _, fromSpec_toSpec _ _ _⟩

Mathlib/AlgebraicGeometry/Sites/Pretopology.lean

@@ -102,15 +102,16 @@ section
 /-- The jointly surjective topology on `Scheme` is defined by the same condition as the jointly
 surjective pretopology. -/
 def jointlySurjectiveTopology : GrothendieckTopology Scheme.{u} :=
-  jointlySurjectivePretopology.toGrothendieck.copy (fun X s ↦ jointlySurjectivePretopology X ↑s) <|
+  jointlySurjectivePretopology.toGrothendieck.copy
+    (fun X ↦ {s | ↑s ∈ jointlySurjectivePretopology X}) <|
     funext fun _ ↦ Set.ext fun s ↦
       ⟨fun ⟨_, hp, hps⟩ x ↦ let ⟨Y, u, hu, hmem⟩ := hp x;
         ⟨Y, u, Presieve.map_monotone hps _ _ hu, hmem⟩,
       fun hs ↦ ⟨s, hs, le_rfl⟩⟩
 
 theorem mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology
     {X : Scheme.{u}} {s : Sieve X} :
-    s ∈ jointlySurjectiveTopology X ↔ jointlySurjectivePretopology X ↑s :=
+    s ∈ jointlySurjectiveTopology X ↔ ↑s ∈ jointlySurjectivePretopology X :=
   Iff.rfl
 
 lemma jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology :

Mathlib/AlgebraicGeometry/Sites/Small.lean

@@ -83,7 +83,7 @@ set_option backward.isDefEq.respectTransparency false in
 /-- The pretopology on `Over S` induced by `P` where coverings are given by `P`-covers
 of `S`-schemes. -/
 def overPretopology : Pretopology (Over S) where
-  coverings Y R := ∃ (𝒰 : Cover.{u} (precoverage P) Y.left) (_ : 𝒰.Over S), R = 𝒰.toPresieveOver
+  coverings Y := {R | ∃ (𝒰 : Cover.{u} (precoverage P) Y.left) (_ : 𝒰.Over S), R = 𝒰.toPresieveOver}
   has_isos {X Y} f _ := ⟨coverOfIsIso f.left, inferInstance, (Presieve.ofArrows_pUnit _).symm⟩
   pullbacks := by
     rintro Y X f _ ⟨𝒰, h, rfl⟩
@@ -179,9 +179,9 @@ are given by `P`-coverings in `S`-schemes satisfying `Q`.
 The most common case is `P = Q`. In this case, this is simply surjective families
 in `S`-schemes with `P`. -/
 def smallPretopology : Pretopology (Q.Over ⊤ S) where
-  coverings Y R :=
-    ∃ (𝒰 : Cover.{u} (precoverage P) Y.left) (_ : 𝒰.Over S) (h : ∀ j : 𝒰.I₀, Q (𝒰.X j ↘ S)),
-      R = 𝒰.toPresieveOverProp h
+  coverings Y :=
+    {R | ∃ (𝒰 : Cover.{u} (precoverage P) Y.left) (_ : 𝒰.Over S) (h : ∀ j : 𝒰.I₀, Q (𝒰.X j ↘ S)),
+      R = 𝒰.toPresieveOverProp h}
   has_isos {X Y} f := ⟨coverOfIsIso f.left, inferInstance, fun _ ↦ Y.prop,
     (Presieve.ofArrows_pUnit _).symm⟩
   pullbacks := by

Mathlib/CategoryTheory/CofilteredSystem.lean

@@ -167,15 +167,15 @@ def toPreimages : J ⥤ Type v where
   map g := MapsTo.restrict (F.map g) _ _ fun x h => by
     rw [mem_iInter] at h ⊢
     intro f
-    rw [← mem_preimage, preimage_preimage, mem_preimage]
-    convert h (g ≫ f); rw [F.map_comp]; rfl
+    simpa using h (g ≫ f)
   map_id j := by
     simp +unfoldPartialApp only [MapsTo.restrict, Subtype.map, F.map_id]
     ext
-    rfl
+    simp
   map_comp f g := by
     simp +unfoldPartialApp only [MapsTo.restrict, Subtype.map, F.map_comp]
-    rfl
+    ext
+    simp
 
 instance toPreimages_finite [∀ j, Finite (F.obj j)] : ∀ j, Finite ((F.toPreimages s).obj j) :=
   fun _ => Subtype.finite

Mathlib/CategoryTheory/Sites/DenseSubsite/InducedTopology.lean

@@ -56,7 +56,7 @@ class LocallyCoverDense : Prop where
 variable [G.LocallyCoverDense K]
 
 theorem pushforward_cover_iff_cover_pullback [G.Full] [G.Faithful] {X : C} (S : Sieve X) :
-    K _ (S.functorPushforward G) ↔ ∃ T : K (G.obj X), T.val.functorPullback G = S := by
+    S.functorPushforward G ∈ K (G.obj X) ↔ ∃ T : K (G.obj X), T.val.functorPullback G = S := by
   constructor
   · intro hS
     exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
@@ -70,10 +70,9 @@ then the set `{ T ∩ mor(C) | T ∈ K }` is a Grothendieck topology of `C`.
 -/
 @[simps]
 def inducedTopology : GrothendieckTopology C where
-  sieves _ S := K _ (S.functorPushforward G)
+  sieves X := {S | S.functorPushforward G ∈ K (G.obj X)}
   top_mem' X := by
-    change K _ _
-    rw [Sieve.functorPushforward_top]
+    rw [Set.mem_setOf, Sieve.functorPushforward_top]
     exact K.top_mem _
   pullback_stable' X Y S iYX hS := by
     apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem
@@ -104,7 +103,7 @@ def inducedTopology : GrothendieckTopology C where
 
 @[simp]
 lemma mem_inducedTopology_sieves_iff {X : C} (S : Sieve X) :
-    S ∈ (G.inducedTopology K) X ↔ (S.functorPushforward G) ∈ K (G.obj X) :=
+    S ∈ G.inducedTopology K X ↔ S.functorPushforward G ∈ K (G.obj X) :=
   Iff.rfl
 
 /-- `G` is cover-lifting w.r.t. the induced topology. -/

Mathlib/CategoryTheory/Sites/Over.lean

@@ -163,18 +163,14 @@ namespace GrothendieckTopology
 /-- The Grothendieck topology on the category `Over X` for any `X : C` that is
 induced by a Grothendieck topology on `C`. -/
 def over (X : C) : GrothendieckTopology (Over X) where
-  sieves Y S := Sieve.overEquiv Y S ∈ J Y.left
-  top_mem' Y := by
-    change _ ∈ J Y.left
-    simp
+  sieves Y := Sieve.overEquiv Y ⁻¹' J Y.left
+  top_mem' Y := by simp
   pullback_stable' Y₁ Y₂ S₁ f h₁ := by
-    change _ ∈ J _ at h₁ ⊢
-    rw [Sieve.overEquiv_pullback]
+    rw [Set.mem_preimage, Sieve.overEquiv_pullback]
     exact J.pullback_stable _ h₁
-  transitive' Y S (hS : _ ∈ J _) R hR := J.transitive hS _ (fun Z f hf => by
-    have hf' : _ ∈ J _ := hR ((Sieve.overEquiv_iff _ _).1 hf)
-    rw [Sieve.overEquiv_pullback] at hf'
-    exact hf')
+  transitive' Y S hS R hR := J.transitive hS _ fun Z f hf => by
+    specialize hR ((Sieve.overEquiv_iff _ _).1 hf)
+    rwa [Set.mem_preimage, Sieve.overEquiv_pullback] at hR
 
 lemma mem_over_iff {X : C} {Y : Over X} (S : Sieve Y) :
     S ∈ (J.over X) Y ↔ Sieve.overEquiv _ S ∈ J Y.left := by

Mathlib/CategoryTheory/Sites/Spaces.lean

@@ -46,7 +46,7 @@ open CategoryTheory TopologicalSpace CategoryTheory.Limits
 
 /-- The Grothendieck topology associated to a topological space. -/
 def grothendieckTopology : GrothendieckTopology (Opens T) where
-  sieves X S := ∀ x ∈ X, ∃ (U : _) (f : U ⟶ X), S f ∧ x ∈ U
+  sieves X := {S | ∀ x ∈ X, ∃ (U : Opens T) (f : U ⟶ X), S f ∧ x ∈ U}
   top_mem' _ _ hx := ⟨_, 𝟙 _, trivial, hx⟩
   pullback_stable' X Y S f hf y hy := by
     rcases hf y (f.le hy) with ⟨U, g, hg, hU⟩
@@ -60,7 +60,7 @@ def grothendieckTopology : GrothendieckTopology (Opens T) where
 set_option backward.isDefEq.respectTransparency false in
 /-- The Grothendieck pretopology associated to a topological space. -/
 def pretopology : Pretopology (Opens T) where
-  coverings X R := ∀ x ∈ X, ∃ (U : _) (f : U ⟶ X), R f ∧ x ∈ U
+  coverings X := {R | ∀ x ∈ X, ∃ (U : _) (f : U ⟶ X), R f ∧ x ∈ U}
   has_isos _ _ f _ _ hx := ⟨_, _, Presieve.singleton_self _, (inv f).le hx⟩
   pullbacks X Y f S hS x hx := by
     rcases hS _ (f.le hx) with ⟨U, g, hg, hU⟩