[Merged by Bors] - chore: fix some Set defeq abuse, golf

Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

@@ -484,7 +484,7 @@ theorem Map.arrows_iff (hφ : Function.Injective φ.obj) (S : Subgroupoid C) {c
 
 /-- The "forward" image of a subgroupoid under a functor injective on objects -/
 def map (hφ : Function.Injective φ.obj) (S : Subgroupoid C) : Subgroupoid D where
-  arrows := Map.Arrows φ hφ S
+  arrows c d := {x | Map.Arrows φ hφ S c d x}
   inv := by
     rintro _ _ _ ⟨⟩
     rw [inv_eq_inv, ← Functor.map_inv, ← inv_eq_inv]
@@ -628,7 +628,7 @@ theorem isTotallyDisconnected_iff :
 
 /-- The isotropy subgroupoid of `S` -/
 def disconnect : Subgroupoid C where
-  arrows c d f := c = d ∧ f ∈ S.arrows c d
+  arrows c d := {f | c = d ∧ f ∈ S.arrows c d}
   inv := by rintro _ _ _ ⟨rfl, h⟩; exact ⟨rfl, S.inv h⟩
   mul := by rintro _ _ _ _ ⟨rfl, h⟩ _ ⟨rfl, h'⟩; exact ⟨rfl, S.mul h h'⟩
 #align category_theory.subgroupoid.disconnect CategoryTheory.Subgroupoid.disconnect
@@ -661,7 +661,7 @@ variable (D : Set C)
 
 /-- The full subgroupoid on a set `D : Set C` -/
 def full : Subgroupoid C where
-  arrows c d _ := c ∈ D ∧ d ∈ D
+  arrows c d := {_f | c ∈ D ∧ d ∈ D}
   inv := by rintro _ _ _ ⟨⟩; constructor <;> assumption
   mul := by rintro _ _ _ _ ⟨⟩ _ ⟨⟩; constructor <;> assumption
 #align category_theory.subgroupoid.full CategoryTheory.Subgroupoid.full

Mathlib/CategoryTheory/IsConnected.lean

@@ -176,13 +176,12 @@ instance [hc : IsConnected J] : IsConnected (ULiftHom.{v₂} (ULift.{u₂} J)) :
   have : Nonempty (ULiftHom.{v₂} (ULift.{u₂} J)) := by simp [ULiftHom, hc.is_nonempty]
   apply IsConnected.of_induct
   rintro p hj₀ h ⟨j⟩
-  let p' : Set J := (fun j : J => p { down := j } : Set J)
+  let p' : Set J := {j : J | p ⟨j⟩}
   have hj₀' : Classical.choice hc.is_nonempty ∈ p' := by
     simp only [(eq_self p')]
     exact hj₀
-  apply
-    induct_on_objects (fun j : J => p { down := j }) hj₀' @fun _ _ f =>
-      h ((ULiftHomULiftCategory.equiv J).functor.map f)
+  apply induct_on_objects p' hj₀' @fun _ _ f =>
+    h ((ULiftHomULiftCategory.equiv J).functor.map f)
 
 /-- Another induction principle for `IsPreconnected J`:
 given a type family `Z : J → Sort*` and
@@ -297,7 +296,7 @@ theorem zag_of_zag_obj (F : J ⥤ K) [Full F] {j₁ j₂ : J} (h : Zag (F.obj j
 theorem equiv_relation [IsConnected J] (r : J → J → Prop) (hr : _root_.Equivalence r)
     (h : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), r j₁ j₂) : ∀ j₁ j₂ : J, r j₁ j₂ := by
   have z : ∀ j : J, r (Classical.arbitrary J) j :=
-    induct_on_objects (fun k => r (Classical.arbitrary J) k) (hr.1 (Classical.arbitrary J))
+    induct_on_objects {k | r (Classical.arbitrary J) k} (hr.1 (Classical.arbitrary J))
       fun f => ⟨fun t => hr.3 t (h f), fun t => hr.3 t (hr.2 (h f))⟩
   intros
   apply hr.3 (hr.2 (z _)) (z _)

Mathlib/Computability/DFA.lean

@@ -92,7 +92,7 @@ theorem evalFrom_of_append (start : σ) (x y : List α) :
 #align DFA.eval_from_of_append DFA.evalFrom_of_append
 
 /-- `M.accepts` is the language of `x` such that `M.eval x` is an accept state. -/
-def accepts : Language α := fun x => M.eval x ∈ M.accept
+def accepts : Language α := {x | M.eval x ∈ M.accept}
 #align DFA.accepts DFA.accepts
 
 theorem mem_accepts (x : List α) : x ∈ M.accepts ↔ M.evalFrom M.start x ∈ M.accept := by rfl

Mathlib/Computability/Language.lean

@@ -45,14 +45,13 @@ variable {l m : Language α} {a b x : List α}
 
 /-- Zero language has no elements. -/
 instance : Zero (Language α) :=
-  ⟨fun _ => False⟩
+  ⟨(∅ : Set _)⟩
 
 /-- `1 : Language α` contains only one element `[]`. -/
 instance : One (Language α) :=
-  ⟨fun l => l = []⟩
+  ⟨{[]}⟩
 
-instance : Inhabited (Language α) :=
-  ⟨fun _ => False⟩
+instance : Inhabited (Language α) := ⟨(∅ : Set _)⟩
 
 /-- The sum of two languages is their union. -/
 instance : Add (Language α) :=

Mathlib/Computability/NFA.lean

@@ -103,7 +103,7 @@ theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.ste
 #align NFA.eval_append_singleton NFA.eval_append_singleton
 
 /-- `M.accepts` is the language of `x` such that there is an accept state in `M.eval x`. -/
-def accepts : Language α := fun x => ∃ S ∈ M.accept, S ∈ M.eval x
+def accepts : Language α := {x | ∃ S ∈ M.accept, S ∈ M.eval x}
 #align NFA.accepts NFA.accepts
 
 theorem mem_accepts : x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x := by rfl

Mathlib/Computability/RegularExpressions.lean

@@ -395,11 +395,8 @@ theorem rmatch_iff_matches' (P : RegularExpression α) :
       tauto
 #align regular_expression.rmatch_iff_matches RegularExpression.rmatch_iff_matches'
 
-instance (P : RegularExpression α) : DecidablePred P.matches' := by
-  intro x
-  change Decidable (x ∈ P.matches')
-  rw [← rmatch_iff_matches']
-  exact instDecidableEqBool (rmatch P x) True
+instance (P : RegularExpression α) : DecidablePred (· ∈ P.matches') := fun _ ↦
+  decidable_of_iff _ (rmatch_iff_matches' _ _)
 
 /-- Map the alphabet of a regular expression. -/
 @[simp]

Mathlib/Data/Set/Finite.lean

@@ -1264,12 +1264,8 @@ theorem card_range_of_injective [Fintype α] {f : α → β} (hf : Injective f)
 #align set.card_range_of_injective Set.card_range_of_injective
 
 theorem Finite.card_toFinset {s : Set α} [Fintype s] (h : s.Finite) :
-    h.toFinset.card = Fintype.card s := by
-  rw [← Finset.card_attach, Finset.attach_eq_univ, ← Fintype.card]
-  refine' Fintype.card_congr (Equiv.setCongr _)
-  ext x
-  show x ∈ h.toFinset ↔ x ∈ s
-  simp
+    h.toFinset.card = Fintype.card s :=
+  Eq.symm <| Fintype.card_of_finset' _ fun _ ↦ h.mem_toFinset
 #align set.finite.card_to_finset Set.Finite.card_toFinset
 
 theorem card_ne_eq [Fintype α] (a : α) [Fintype { x : α | x ≠ a }] :

Mathlib/Data/Set/Image.lean

@@ -507,7 +507,6 @@ theorem image_inter_preimage (f : α → β) (s : Set α) (t : Set β) :
   · calc
       f '' (s ∩ f ⁻¹' t) ⊆ f '' s ∩ f '' (f ⁻¹' t) := image_inter_subset _ _ _
       _ ⊆ f '' s ∩ t := inter_subset_inter_right _ (image_preimage_subset f t)
-
   · rintro _ ⟨⟨x, h', rfl⟩, h⟩
     exact ⟨x, ⟨h', h⟩, rfl⟩
 #align set.image_inter_preimage Set.image_inter_preimage

Mathlib/GroupTheory/Congruence.lean

@@ -879,16 +879,11 @@ theorem mrange_mk' : MonoidHom.mrange c.mk' = ⊤ :=
 #align con.mrange_mk' Con.mrange_mk'
 #align add_con.mrange_mk' AddCon.mrange_mk'
 
-/-- The elements related to `x ∈ M`, `M` a monoid, by the kernel of a monoid homomorphism are
-    those in the preimage of `f(x)` under `f`. -/
-@[to_additive "The elements related to `x ∈ M`, `M` an `AddMonoid`, by the kernel of
-an `AddMonoid` homomorphism are those in the preimage of `f(x)` under `f`. "]
-theorem ker_apply_eq_preimage {f : M →* P} (x) : (ker f) x = f ⁻¹' {f x} :=
-  Set.ext fun _ =>
-    ⟨fun h => Set.mem_preimage.2 <| Set.mem_singleton_iff.2 h.symm, fun h =>
-      (Set.mem_singleton_iff.1 <| Set.mem_preimage.1 h).symm⟩
-#align con.ker_apply_eq_preimage Con.ker_apply_eq_preimage
-#align add_con.ker_apply_eq_preimage AddCon.ker_apply_eq_preimage
+-- Porting note: used to abuse defeq between sets and predicates
+@[to_additive]
+theorem ker_apply {f : M →* P} {x y} : ker f x y ↔ f x = f y := Iff.rfl
+#noalign con.ker_apply_eq_preimage
+#noalign add_con.ker_apply_eq_preimage
 
 /-- Given a monoid homomorphism `f : N → M` and a congruence relation `c` on `M`, the congruence
     relation induced on `N` by `f` equals the kernel of `c`'s quotient homomorphism composed with

Mathlib/GroupTheory/Submonoid/Basic.lean

@@ -173,20 +173,19 @@ theorem mem_carrier {s : Submonoid M} {x : M} : x ∈ s.carrier ↔ x ∈ s :=
 #align add_submonoid.mem_carrier AddSubmonoid.mem_carrier
 
 @[to_additive (attr := simp)]
-theorem mem_mk {s : Set M} {x : M} (h_one) (h_mul) : x ∈ mk ⟨s, h_mul⟩ h_one ↔ x ∈ s :=
+theorem mem_mk {s : Subsemigroup M} {x : M} (h_one) : x ∈ mk s h_one ↔ x ∈ s :=
   Iff.rfl
 #align submonoid.mem_mk Submonoid.mem_mk
 #align add_submonoid.mem_mk AddSubmonoid.mem_mk
 
 @[to_additive (attr := simp)]
-theorem coe_set_mk {s : Set M} (h_one) (h_mul) : (mk ⟨s, h_mul⟩ h_one : Set M) = s :=
+theorem coe_set_mk {s : Subsemigroup M} (h_one) : (mk s h_one : Set M) = s :=
   rfl
 #align submonoid.coe_set_mk Submonoid.coe_set_mk
 #align add_submonoid.coe_set_mk AddSubmonoid.coe_set_mk
 
 @[to_additive (attr := simp)]
-theorem mk_le_mk {s t : Set M} (h_one) (h_mul) (h_one') (h_mul') :
-    mk ⟨s, h_mul⟩ h_one ≤ mk ⟨t, h_mul'⟩ h_one' ↔ s ⊆ t :=
+theorem mk_le_mk {s t : Subsemigroup M} (h_one) (h_one') : mk s h_one ≤ mk t h_one' ↔ s ≤ t :=
   Iff.rfl
 #align submonoid.mk_le_mk Submonoid.mk_le_mk
 #align add_submonoid.mk_le_mk AddSubmonoid.mk_le_mk

Mathlib/Logic/Equiv/Set.lean

@@ -198,7 +198,6 @@ def image {α β : Type _} (e : α ≃ β) (s : Set α) :
 
 namespace Set
 
-
 --Porting note: Removed attribute @[simps apply symm_apply]
 /-- `univ α` is equivalent to `α`. -/
 protected def univ (α) : @univ α ≃ α :=

Mathlib/Logic/Function/Basic.lean

@@ -271,19 +271,18 @@ theorem Bijective.of_comp_iff' {f : α → β} (hf : Bijective f) (g : γ → α
 /-- **Cantor's diagonal argument** implies that there are no surjective functions from `α`
 to `Set α`. -/
 theorem cantor_surjective {α} (f : α → Set α) : ¬Surjective f
-  | h => let ⟨D, e⟩ := h (λ a => ¬ f a a)
-        (@iff_not_self (f D D)) $ iff_of_eq (congr_fun e D)
+  | h => let ⟨D, e⟩ := h {a | ¬ f a a}
+        @iff_not_self (D ∈ f D) <| iff_of_eq <| congr_arg (D ∈ ·) e
 #align function.cantor_surjective Function.cantor_surjective
 
 /-- **Cantor's diagonal argument** implies that there are no injective functions from `Set α`
 to `α`. -/
 theorem cantor_injective {α : Type _} (f : Set α → α) : ¬Injective f
-  | i => cantor_surjective (λ a b => ∀ U, a = f U → U b) $
-        RightInverse.surjective
-          (λ U => funext $ λ _a => propext ⟨λ h => h U rfl, λ h' _U e => i e ▸ h'⟩)
+  | i => cantor_surjective (fun a ↦ {b | ∀ U, a = f U → U b}) <|
+         RightInverse.surjective (λ U => Set.ext <| fun _ ↦ ⟨fun h ↦ h U rfl, fun h _ e ↦ i e ▸ h⟩)
 #align function.cantor_injective Function.cantor_injective
 
-/-- There is no surjection from `α : Type u` into `Type u`. This theorem
+/-- There is no surjection from `α : Type u` into `Type (max u v)`. This theorem
   demonstrates why `Type : Type` would be inconsistent in Lean. -/
 theorem not_surjective_Type {α : Type u} (f : α → Type max u v) : ¬Surjective f := by
   intro hf

Mathlib/Order/Closure.lean

@@ -166,7 +166,7 @@ theorem le_closure_iff (x y : α) : x ≤ c y ↔ c x ≤ c y :=
 #align closure_operator.le_closure_iff ClosureOperator.le_closure_iff
 
 /-- An element `x` is closed for the closure operator `c` if it is a fixed point for it. -/
-def closed : Set α := fun x => c x = x
+def closed : Set α := {x | c x = x}
 #align closure_operator.closed ClosureOperator.closed
 
 theorem mem_closed_iff (x : α) : x ∈ c.closed ↔ c x = x :=
@@ -380,7 +380,7 @@ section Preorder
 variable [Preorder α] [Preorder β] {u : β → α} (l : LowerAdjoint u)
 
 /-- An element `x` is closed for `l : LowerAdjoint u` if it is a fixed point: `u (l x) = x` -/
-def closed : Set α := fun x => u (l x) = x
+def closed : Set α := {x | u (l x) = x}
 #align lower_adjoint.closed LowerAdjoint.closed
 
 theorem mem_closed_iff (x : α) : x ∈ l.closed ↔ u (l x) = x :=

Mathlib/Order/CountableDenseLinearOrder.lean

@@ -142,7 +142,7 @@ variable (β)
     partial isomorphism can be extended to one defined at `a`. -/
 def definedAtLeft [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] (a : α) :
     Cofinal (PartialIso α β) where
-  carrier f := ∃ b : β, (a, b) ∈ f.val
+  carrier := {f | ∃ b : β, (a, b) ∈ f.val}
   mem_gt f := by
     cases' exists_across f a with b a_b
     refine
@@ -163,7 +163,7 @@ variable (α) {β}
     partial isomorphism can be extended to include `b`. We prove this by symmetry. -/
 def definedAtRight [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α] (b : β) :
     Cofinal (PartialIso α β) where
-  carrier f := ∃ a, (a, b) ∈ f.val
+  carrier := {f | ∃ a, (a, b) ∈ f.val}
   mem_gt f := by
     rcases (definedAtLeft α b).mem_gt f.comm with ⟨f', ⟨a, ha⟩, hl⟩
     refine' ⟨f'.comm, ⟨a, _⟩, _⟩