refactor(Data): make Set a one-field structure

Archive/Imo/Imo1987Q1.lean

@@ -54,7 +54,7 @@ fixed points. -/
 def fiber (k : ℕ) : Set (Perm α) :=
   {σ : Perm α | card (fixedPoints σ) = k}
 
-instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (setOf _)
+instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (Set.ofPred _)
 
 @[simp]
 theorem mem_fiber {σ : Perm α} {k : ℕ} : σ ∈ fiber α k ↔ card (fixedPoints σ) = k :=

Archive/Imo/Imo1988Q6.lean

@@ -92,7 +92,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   -- Our assumptions ensure that we can then prove the claim.
   suffices exc : exceptional.Nonempty by
     -- Suppose that there exists an element in the exceptional locus.
-    simp only [Set.Nonempty, Prod.exists, Set.mem_setOf_eq, exceptional] at exc
+    simp only [Set.Nonempty, Prod.exists, Set.mem_ofPred_eq, exceptional] at exc
     -- Let (a,b) be such an element, and consider all the possible cases.
     rcases exc with ⟨a, b, hH, hb⟩
     rcases hb with (_ | rfl | rfl | hB | hB)
@@ -138,7 +138,7 @@ theorem constant_descent_vieta_jumping (x y : ℕ) {claim : Prop} {H : ℕ → 
   -- This means that m_y = m,
   -- and the conditions H(m_x, m_y) and m_x < m_y are satisfied.
   simp only at mx_lt_my hHm m_eq
-  simp only [exceptional, hHm, Set.mem_setOf_eq, true_and] at h_base
+  simp only [exceptional, hHm, Set.mem_ofPred_eq, true_and] at h_base
   push Not at h_base
   -- Finally, it also means that (m_x, m_y) does not lie in the base locus,
   -- that m_x ≠ 0, m_x ≠ m_y, B(m_x) ≠ m_y, and B(m_x) ≠ m_x + m_y.

Archive/Imo/Imo2008Q2.lean

@@ -65,7 +65,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
   have hW_sub_S : W ⊆ rationalSolutions := by
     intro s hs_in_W
     rw [rationalSolutions]
-    simp only [Set.mem_setOf_eq] at hs_in_W ⊢
+    simp only [Set.mem_ofPred_eq] at hs_in_W ⊢
     rcases hs_in_W with ⟨x, y, z, h₁, t, ht_gt_zero, hx_t, hy_t, hz_t⟩
     use x, y, z
     have key_gt_zero : 0 < t ^ 2 + t + 1 := by linarith [pow_pos ht_gt_zero 2, ht_gt_zero]
@@ -99,7 +99,7 @@ theorem imo2008_q2b : Set.Infinite rationalSolutions := by
         set z : ℚ := -t * (t + 1) with hz_def
         simp only [t, W, K, g, Set.mem_image, Prod.exists]
         use x, y, z; constructor
-        · simp only [Set.mem_setOf_eq]
+        · simp only [Set.mem_ofPred_eq]
           use x, y, z; constructor
           · rfl
           · use t; constructor

Archive/Imo/Imo2024Q5.lean

@@ -1034,7 +1034,7 @@ def answer : ℕ := 3
 
 /-- The final result, combining upper and lower bounds. -/
 theorem result : IsLeast {k | ∃ s : Strategy 2022, s.ForcesWinIn k} answer := by
-  simp_rw [IsLeast, mem_lowerBounds, Set.mem_setOf, forall_exists_index]
+  simp_rw [IsLeast, mem_lowerBounds, Set.mem_ofPred, forall_exists_index]
   exact ⟨⟨winningStrategy (by simp), winningStrategy_forcesWinIn_three (by simp)⟩,
     fun k s h ↦ h.three_le (by simp)⟩
 

Archive/Sensitivity.lean

@@ -140,7 +140,7 @@ theorem adj_iff_proj_adj {p q : Q n.succ} (h₀ : p 0 = q 0) :
 
 @[symm]
 theorem adjacent.symm {p q : Q n} : q ∈ p.adjacent ↔ p ∈ q.adjacent := by
-  simp only [adjacent, ne_comm, Set.mem_setOf_eq]
+  simp only [adjacent, ne_comm, Set.mem_ofPred_eq]
 
 end Q
 

Archive/Wiedijk100Theorems/AreaOfACircle.lean

@@ -65,7 +65,7 @@ theorem disc_eq_regionBetween :
       regionBetween
         (fun x => -sqrt (r ^ 2 - x ^ 2)) (fun x => sqrt (r ^ 2 - x ^ 2)) (Ioc (-r) r) := by
   ext p
-  simp only [disc, regionBetween, mem_setOf_eq, mem_Ioo, mem_Ioc]
+  simp only [disc, regionBetween, mem_ofPred_eq, mem_Ioo, mem_Ioc]
   constructor <;> intro h
   · cases abs_lt_of_sq_lt_sq' (lt_of_add_lt_of_nonneg_left h (sq_nonneg p.2)) r.2 with
     | intro left right =>

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -74,7 +74,7 @@ open scoped List in
 theorem mem_countedSequence_iff_perm {p q l} :
     l ∈ countedSequence p q ↔ l ~ List.replicate p (1 : ℤ) ++ List.replicate q (-1) := by
   rw [List.perm_replicate_append_replicate]
-  · simp only [countedSequence, List.subset_def, mem_setOf_eq, List.mem_cons (b := (1 : ℤ)),
+  · simp only [countedSequence, List.subset_def, mem_ofPred_eq, List.mem_cons (b := (1 : ℤ)),
       List.mem_singleton]
   · norm_num1
 
@@ -200,7 +200,7 @@ theorem first_vote_pos :
         ((countedSequence_nonempty _ _).image _)]
     · have : List.cons (-1) '' countedSequence (p + 1) q ∩ {l : List ℤ | l.headI = 1} = ∅ := by
         ext
-        simp only [mem_inter_iff, mem_image, mem_setOf_eq, mem_empty_iff_false, iff_false,
+        simp only [mem_inter_iff, mem_image, mem_ofPred_eq, mem_empty_iff_false, iff_false,
           not_and, forall_exists_index, and_imp]
         rintro l _ rfl
         norm_num
@@ -255,7 +255,7 @@ theorem countedSequence_int_pos_counted_succ_succ (p q : ℕ) :
   rw [counted_succ_succ, union_inter_distrib_right,
       (_ : List.cons (-1) '' countedSequence (p + 1) q ∩ {l | l.headI = 1} = ∅), union_empty] <;>
     · ext
-      simp only [mem_inter_iff, mem_image, mem_setOf_eq, and_iff_left_iff_imp, mem_empty_iff_false,
+      simp only [mem_inter_iff, mem_image, mem_ofPred_eq, and_iff_left_iff_imp, mem_empty_iff_false,
         iff_false, not_and, forall_exists_index, and_imp]
       rintro y _ rfl
       norm_num

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -50,7 +50,7 @@ theorem birthday_measure :
     trans ‖Fin 23 ↪ Fin 365‖
     · rw [← Fintype.card_coe]
       apply Fintype.card_congr
-      rw [Set.Finite.coeSort_toFinset, Set.coe_setOf]
+      rw [Set.Finite.coeSort_toFinset, Set.coe_ofPred]
       exact Equiv.subtypeInjectiveEquivEmbedding _ _
     · rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin]
       rfl

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -183,7 +183,7 @@ theorem shiftUp_bottom_subset_bottoms (hc : (cs i).xm ≠ 1) :
     (cs i).shiftUp.bottom ⊆ ⋃ i : ι, (cs i).bottom := by
   intro p hp; obtain ⟨hp0, hps⟩ := hp; rw [tail_shiftUp] at hps
   have : p ∈ (unitCube : Cube (n + 1)).toSet := by
-    simp only [toSet, forall_iff_succ, hp0, side_unitCube, mem_setOf_eq, mem_Ico, head_shiftUp]
+    simp only [toSet, forall_iff_succ, hp0, side_unitCube, mem_ofPred_eq, mem_Ico, head_shiftUp]
     refine ⟨⟨?_, ?_⟩, ?_⟩
     · rw [← zero_add (0 : ℝ)]; apply add_le_add
       · apply zero_le_b h
@@ -223,10 +223,10 @@ variable {c : Cube (n + 1)} (h : Correct cs) (v : Valley cs c)
 theorem valley_unitCube [Nontrivial ι] (h : Correct cs) : Valley cs unitCube := by
   refine ⟨?_, ?_, ?_⟩
   · intro v
-    simp only [bottom, and_imp, mem_iUnion, mem_setOf_eq]
+    simp only [bottom, and_imp, mem_iUnion, mem_ofPred_eq]
     intro h0 hv
     have : v ∈ (unitCube : Cube (n + 1)).toSet := by
-      dsimp only [toSet, unitCube, mem_setOf_eq]
+      dsimp only [toSet, unitCube, mem_ofPred_eq]
       rw [forall_iff_succ, h0]; constructor
       · norm_num [side, unitCube]
       · exact hv
@@ -410,7 +410,7 @@ theorem mi_not_onBoundary (j : Fin n) : ¬OnBoundary (mi_mem_bcubes : mi h v ∈
   have i'_i'' : i' ≠ i'' := by
     rintro ⟨⟩
     have : (cs i).b ∈ (cs i').toSet := by
-      simp only [toSet, forall_iff_succ, hi.1, bottom_mem_side h2i', true_and, mem_setOf_eq]
+      simp only [toSet, forall_iff_succ, hi.1, bottom_mem_side h2i', true_and, mem_ofPred_eq]
       intro j₂; by_cases hj₂ : j₂ = j
       · simpa [p', side_tail, hj'.symm, hj₂] using hi''.2 j
       · simpa [p, hj₂] using! hi'.2 j₂
@@ -457,7 +457,7 @@ theorem valley_mi : Valley cs (cs (mi h v)).shiftUp := by
     simp only [not_subset, tail_shiftUp] at h2i'
     rcases h2i' with ⟨p1, hp1, h2p1⟩
     have : ∃ p3, p3 ∈ (cs i').tail.toSet ∧ p3 ∉ (cs i).tail.toSet ∧ p3 ∈ c.tail.toSet := by
-      simp only [toSet, not_forall, mem_setOf_eq] at h2p1; obtain ⟨j, hj⟩ := h2p1
+      simp only [toSet, not_forall, mem_ofPred_eq] at h2p1; obtain ⟨j, hj⟩ := h2p1
       rcases Ico_lemma (mi_not_onBoundary' j).1 (by simp [hw]) (mi_not_onBoundary' j).2
           (le_trans (hp2 j).1 <| le_of_lt (h2p2 j).2) (le_trans (h2p2 j).1 <| le_of_lt (hp2 j).2)
           ⟨hj, hp1 j⟩ with
@@ -466,7 +466,7 @@ theorem valley_mi : Valley cs (cs (mi h v)).shiftUp := by
       · intro j'; by_cases h : j' = j
         · simp only [if_pos h]; exact h ▸ h3w
         · simp only [if_neg h]; exact hp2 j'
-      · simp only [toSet, not_forall, mem_setOf_eq]; use j; rw [if_pos rfl]; convert! h2w
+      · simp only [toSet, not_forall, mem_ofPred_eq]; use j; rw [if_pos rfl]; convert! h2w
       · intro j'; by_cases h : j' = j
         · simp only [if_pos h, side_tail]; exact h ▸ hw
         · simp only [if_neg h]; apply hi.2; apply h2p2
@@ -484,7 +484,7 @@ theorem valley_mi : Valley cs (cs (mi h v)).shiftUp := by
     let p' := @cons n (fun _ => ℝ) (cs i).xm p3
     have hp' : p' ∈ (cs i').toSet := by simpa [i, p', toSet, forall_iff_succ, hi'.symm] using! h1p3
     have h2p' : p' ∈ (cs i'').toSet := by
-      simp only [p', toSet, forall_iff_succ, cons_succ, cons_zero, mem_setOf_eq]
+      simp only [p', toSet, forall_iff_succ, cons_succ, cons_zero, mem_ofPred_eq]
       refine ⟨?_, by simpa [toSet] using! hi''.2⟩
       have : (cs i).b 0 = (cs i'').b 0 := by rw [hi.1, h2i''.1]
       simp [side, hw', xm, this, h3i'']

Archive/Wiedijk100Theorems/Konigsberg.lean

@@ -66,15 +66,17 @@ lemma degree_eq_degree (v : Verts) : graph.degree v = degree v := by cases v <;>
 lemma not_even_degree_iff (w : Verts) : ¬Even (degree w) ↔ w = V1 ∨ w = V2 ∨ w = V3 ∨ w = V4 := by
   cases w <;> decide
 
-lemma setOf_odd_degree_eq :
+lemma setOfPred_odd_degree_eq :
     {v | Odd (graph.degree v)} = {Verts.V1, Verts.V2, Verts.V3, Verts.V4} := by
   ext w
   simp [not_even_degree_iff, ← Nat.not_even_iff_odd]
 
+@[deprecated (since := "2026-07-09")] alias setOf_odd_degree_eq := setOfPred_odd_degree_eq
+
 /-- The Königsberg graph is not Eulerian. -/
 theorem not_isEulerian {u v : Verts} (p : graph.Walk u v) (h : p.IsEulerian) : False := by
   have h := h.card_odd_degree
-  have h' := setOf_odd_degree_eq
+  have h' := setOfPred_odd_degree_eq
   apply_fun Fintype.card at h'
   rw [h'] at h
   simp at h

Archive/ZagierTwoSquares.lean

@@ -38,7 +38,7 @@ variable (k : ℕ) [hk : Fact (4 * k + 1).Prime]
 def zagierSet : Set (ℕ × ℕ × ℕ) := {t | t.1 * t.1 + 4 * t.2.1 * t.2.2 = 4 * k + 1}
 
 lemma zagierSet_lower_bound {x y z : ℕ} (h : (x, y, z) ∈ zagierSet k) : 0 < x ∧ 0 < y ∧ 0 < z := by
-  rw [zagierSet, mem_setOf_eq] at h
+  rw [zagierSet, mem_ofPred_eq] at h
   refine ⟨?_, ?_, ?_⟩
   all_goals
     by_contra q
@@ -57,7 +57,7 @@ lemma zagierSet_lower_bound {x y z : ℕ} (h : (x, y, z) ∈ zagierSet k) : 0 <
 lemma zagierSet_upper_bound {x y z : ℕ} (h : (x, y, z) ∈ zagierSet k) :
     x ≤ k + 1 ∧ y ≤ k ∧ z ≤ k := by
   obtain ⟨_, _, _⟩ := zagierSet_lower_bound k h
-  rw [zagierSet, mem_setOf_eq] at h
+  rw [zagierSet, mem_ofPred_eq] at h
   refine ⟨?_, ?_, ?_⟩ <;> nlinarith
 
 lemma zagierSet_subset : zagierSet k ⊆ Ioc 0 (k + 1) ×ˢ Ioc 0 k ×ˢ Ioc 0 k := by
@@ -80,7 +80,7 @@ variable (k : ℕ)
 
 /-- The obvious involution `(x, y, z) ↦ (x, z, y)`. -/
 def obvInvo : Function.End (zagierSet k) := fun ⟨⟨x, y, z⟩, h⟩ => ⟨⟨x, z, y⟩, by
-  simp only [zagierSet, Set.mem_setOf_eq] at h ⊢
+  simp only [zagierSet, Set.mem_ofPred_eq] at h ⊢
   linarith [h]⟩
 
 theorem obvInvo_sq : obvInvo k ^ 2 = 1 := rfl
@@ -93,7 +93,7 @@ theorem sq_add_sq_of_nonempty_fixedPoints (hn : (fixedPoints (obvInvo k)).Nonemp
   obtain ⟨⟨⟨x, y, z⟩, he⟩, hf⟩ := hn
   have := mem_fixedPoints_iff.mp hf
   simp only [obvInvo, Subtype.mk.injEq, Prod.mk.injEq, true_and] at this
-  simp only [zagierSet, Set.mem_setOf_eq] at he
+  simp only [zagierSet, Set.mem_ofPred_eq] at he
   use x, (2 * y)
   rw [show 2 * y * (2 * y) = 4 * y * y by linarith, ← he, this.1]
 
@@ -103,7 +103,7 @@ def complexInvo : Function.End (zagierSet k) := fun ⟨⟨x, y, z⟩, h⟩ =>
   ⟨if x + z < y then ⟨x + 2 * z, z, y - x - z⟩ else
    if 2 * y < x then ⟨x - 2 * y, x + z - y, y⟩ else
                      ⟨2 * y - x, y, x + z - y⟩, by
-  split_ifs with less more <;> simp only [zagierSet, Set.mem_setOf_eq] at h ⊢
+  split_ifs with less more <;> simp only [zagierSet, Set.mem_ofPred_eq] at h ⊢
   · -- less: `x + z < y` (`x < y - z` as stated by Zagier)
     rw [Nat.sub_sub]; zify [less.le] at h ⊢; linarith [h]
   · -- more: `2 * y < x`
@@ -152,7 +152,7 @@ theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (comple
   · -- more
     obtain ⟨_, _, _⟩ := mem; simp_all
   · -- middle (the one fixed point falls under this case)
-    simp only [zagierSet, Set.mem_setOf_eq] at h
+    simp only [zagierSet, Set.mem_ofPred_eq] at h
     replace mem := mem.1
     rw [tsub_eq_iff_eq_add_of_le more, ← two_mul] at mem
     replace mem := (mul_left_cancel₀ two_ne_zero mem).symm
@@ -167,7 +167,7 @@ theorem eq_of_mem_fixedPoints {t : zagierSet k} (mem : t ∈ fixedPoints (comple
 
 /-- The singleton containing `(1, 1, k)`. -/
 def singletonFixedPoint : Finset (zagierSet k) :=
-  {⟨(1, 1, k), (by simp only [zagierSet, Set.mem_setOf_eq]; linarith)⟩}
+  {⟨(1, 1, k), (by simp only [zagierSet, Set.mem_ofPred_eq]; linarith)⟩}
 
 /-- `complexInvo k` has exactly one fixed point. -/
 theorem card_fixedPoints_eq_one : Fintype.card (fixedPoints (complexInvo k)) = 1 := by

Counterexamples/AharoniKorman.lean

@@ -243,7 +243,7 @@ This corresponds to 5.8 (i) in the [hollom2025].
 -/
 lemma ordConnected_level {n : ℕ} : (level n).OrdConnected := by
   rw [Set.ordConnected_iff]
-  simp only [level_eq, Set.mem_setOf_eq, Set.subset_def, Set.mem_Icc, and_imp, Hollom.forall,
+  simp only [level_eq, Set.mem_ofPred_eq, Set.subset_def, Set.mem_Icc, and_imp, Hollom.forall,
     Prod.forall, forall_eq, toHollom_le_toHollom_iff_fixed_right]
   intro a b c d ac bd e f g h1 h2
   exact le_antisymm (le_of_toHollom_le_toHollom h1) (le_of_toHollom_le_toHollom h2)
@@ -415,7 +415,7 @@ theorem exists_finite_intersection (hC : IsChain (· ≤ ·) C) :
   -- In fact, we only need it to be nonempty, and find a point.
   obtain ⟨x, hxy⟩ := this.nonempty
   induction hxy.1.2 using induction_on_level with | h x y =>
-  simp only [Set.mem_sdiff, Set.mem_inter_iff, toHollom_mem_level_iff, and_true, Set.mem_setOf_eq,
+  simp only [Set.mem_sdiff, Set.mem_inter_iff, toHollom_mem_level_iff, and_true, Set.mem_ofPred_eq,
     not_le, D] at hxy
   -- Take the point `(x, y, n + 1)` in `C` that avoids `D`. As `(u, v, n)` is also in the chain `C`,
   -- they must be comparable.
@@ -840,7 +840,7 @@ lemma square_subset_above (h : (C ∩ level n).Finite) :
   simp +contextual only [sup_le_iff, embed, RelEmbedding.coe_mk,
     Function.Embedding.coeFn_mk, Set.mem_inter_iff, and_imp, «forall», toHollom_mem_level_iff,
     Prod.forall, Set.subset_def, Set.mem_image, Set.mem_Ici, Prod.exists, Prod.mk_le_mk,
-    Set.mem_setOf_eq, forall_exists_index, Prod.mk.injEq,
+    Set.mem_ofPred_eq, forall_exists_index, Prod.mk.injEq,
     toHollom_le_toHollom_iff_fixed_right, Set.mem_sdiff, and_true, ← max_add_add_right,
     Hollom.ext_iff]
   -- After simplifying, direct calculations show the subset relation as required.
@@ -956,7 +956,7 @@ lemma square_subset_S_case_1 (h : (C ∩ level n).Finite) (h' : (C ∩ level (n
     rw [eventually_atTop, level_eq]
     refine ⟨max b c, ?_⟩
     simp only [sup_le_iff, embed, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
-      Set.mem_inter_iff, Set.mem_setOf_eq, and_imp, «forall», Prod.forall,
+      Set.mem_inter_iff, Set.mem_ofPred_eq, and_imp, «forall», Prod.forall,
       Set.subset_def, Set.mem_image, Set.mem_Ici, Prod.exists, Prod.mk_le_mk, forall_exists_index,
       Prod.mk.injEq, Hollom.ext_iff]
     rintro d hbd hcd _ _ _ e f hde hdf rfl rfl rfl g h _ hgh rfl
@@ -1027,18 +1027,18 @@ theorem not_S_hits_next (f : SpinalMap C) (hC : IsChain (· ≤ ·) C)
   cases (C ∩ level (n + 1)).finite_or_infinite
   -- In the case that `C ∩ level (n + 1)` is finite, this is immediate from the definition of `S`.
   case inl h =>
-    rw [S, if_pos h, Set.mem_setOf_eq] at hx
+    rw [S, if_pos h, Set.mem_ofPred_eq] at hx
     intro hy
     refine f.incomp_apply ?_ (hx.2 _ hy).symm
     have := R_subset_level hx.1
-    simp only [level_eq, Set.mem_setOf_eq] at this
+    simp only [level_eq, Set.mem_ofPred_eq] at this
     intro h
     simp [level_eq, h, this] at hy
   -- So suppose it is infinite
   case inr h =>
     -- Write `(x, y, n)` for our given point, and set `(a, b, n + 1) := f(x, y, n)`
     induction S_subset_level hx using induction_on_level with | h x y =>
-    simp only [S, if_neg h, Set.mem_setOf_eq] at hx
+    simp only [S, if_neg h, Set.mem_ofPred_eq] at hx
     intro hp
     set fp := f h(x, y, n) with hfp
     clear_value fp

Counterexamples/Phillips.lean

@@ -460,7 +460,7 @@ We need the continuum hypothesis to construct it.
 theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
     ∃ f : ℝ → Set ℝ, (∀ x, (univ \ f x).Countable) ∧ ∀ y, {x : ℝ | y ∈ f x}.Countable := by
   obtain ⟨r, hr₁, hr₂⟩ := Cardinal.exists_rel_mk_fibers_lt ℝ
-  refine ⟨fun x ↦ setOf (r x), ?_, ?_⟩
+  refine ⟨fun x ↦ Set.ofPred (r x), ?_, ?_⟩
   · simpa [Hcont, ← Set.compl_eq_univ_sdiff] using! hr₁
   · simpa [Hcont] using hr₂
 
@@ -512,15 +512,15 @@ theorem countable_ne (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ)
     {x | φ.toBoundedAdditiveMeasure.continuousPart univ ≠ φ (f Hcont x)} ⊆
       {x | (φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x).Nonempty} := by
     intro x hx
-    simp only [mem_setOf] at *
+    simp only [mem_ofPred] at *
     contrapose! hx
     exact apply_f_eq_continuousPart Hcont φ x hx |>.symm
   have B :
     {x | (φ.toBoundedAdditiveMeasure.discreteSupport ∩ spf Hcont x).Nonempty} ⊆
       ⋃ y ∈ φ.toBoundedAdditiveMeasure.discreteSupport, {x | y ∈ spf Hcont x} := by
     intro x hx
     dsimp at hx
-    simp only [exists_prop, mem_iUnion, mem_setOf_eq]
+    simp only [exists_prop, mem_iUnion, mem_ofPred_eq]
     exact hx
   apply Countable.mono (Subset.trans A B)
   exact Countable.biUnion (countable_discreteSupport _) fun a _ => countable_spf_mem Hcont a
@@ -531,7 +531,7 @@ theorem comp_ae_eq_const (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ
   apply ae_restrict_of_ae
   refine measure_mono_null ?_ ((countable_ne Hcont φ).measure_zero _)
   intro x
-  simp only [imp_self, mem_setOf_eq, mem_compl_iff]
+  simp only [imp_self, mem_ofPred_eq, mem_compl_iff]
 
 theorem integrable_comp (Hcont : #ℝ = ℵ₁) (φ : (DiscreteCopy ℝ →ᵇ ℝ) →L[ℝ] ℝ) :
     IntegrableOn (fun x => φ (f Hcont x)) (Icc 0 1) := by

Counterexamples/SeparableNotSecondCountable.lean

@@ -45,7 +45,7 @@ theorem not_secondCountableTopology : ¬SecondCountableTopology (ℝ ×ₗ Bool)
   intro h
   have : {x : ℝ ×ₗ Bool | (ofLex x).2}.Countable := by
     simpa [Prod.Lex.covBy_iff, Bool.covBy_iff, exists_or, not_covBy, (Bool.le_true _).not_gt,
-      (Bool.false_le _).lt_iff_ne] using countable_setOf_covBy_left (α := ℝ ×ₗ Bool)
+      (Bool.false_le _).lt_iff_ne] using countable_setOfPred_covBy_left (α := ℝ ×ₗ Bool)
   refine not_countable_univ <| (this.image fun x ↦ (ofLex x).1).mono fun x _ ↦ ?_
   exact ⟨toLex (x, true), rfl, rfl⟩
 

Counterexamples/SorgenfreyLine.lean

@@ -71,7 +71,7 @@ theorem nhds_basis_Ico (a : ℝₗ) : (𝓝 a).HasBasis (a < ·) (Ico a ·) := b
   have : (⨅ x : { i // i ≤ a }, 𝓟 (Ici ↑x)) = 𝓟 (Ici a) := by
     refine (IsLeast.isGLB ?_).iInf_eq
     exact ⟨⟨⟨a, le_rfl⟩, rfl⟩, forall_mem_range.2 fun b => principal_mono.2 <| Ici_subset_Ici.2 b.2⟩
-  simp only [mem_setOf_eq, iInf_and, iInf_exists, @iInf_comm _ (_ ∈ _), @iInf_comm _ (Set ℝₗ),
+  simp only [mem_ofPred_eq, iInf_and, iInf_exists, @iInf_comm _ (_ ∈ _), @iInf_comm _ (Set ℝₗ),
     iInf_iInf_eq_right, mem_Ico]
   simp_rw [@iInf_comm _ ℝₗ (_ ≤ _), iInf_subtype', ← Ici_inter_Iio, ← inf_principal,
     ← inf_iInf, ← iInf_inf, this, iInf_subtype]
@@ -281,7 +281,7 @@ theorem not_separatedNhds_rat_irrational_antidiag :
   have H : {x : ℝ | Irrational x} ⊆ ⋃ n, C n := fun x hx =>
     mem_iUnion.2 ⟨_, subset_closure ⟨hx, rfl⟩⟩
   have Hd : Dense (⋃ n, interior (C n)) :=
-    IsGδ.setOf_irrational.dense_iUnion_interior_of_closed dense_irrational
+    IsGδ.setOfPred_irrational.dense_iUnion_interior_of_closed dense_irrational
       (fun _ => isClosed_closure) H
   obtain ⟨N, hN⟩ : ∃ n : ℕ+, (interior <| C n).Nonempty := nonempty_iUnion.mp Hd.nonempty
   /- Choose a rational number `r` in the interior of the closure of `C N`, then choose `n ≥ N > 0`