chore(Data): rename setOf to Set.ofPred (#41507)

This is in prevision of making `Set` a one-field structure. `ofPred` will then be the constructor.

Generated by Claude Opus then reviewed line-by-line by myself.

Assisted-by: Claude Opus 4.8

Author: YaelDillies

Archive/Imo/Imo1987Q1.lean

@@ -56,7 +56,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/Imo2024Q3.lean

@@ -1042,7 +1042,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/Imo/Imo2024Q5.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/Sensitivity.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/AreaOfACircle.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/BallotProblem.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/BirthdayProblem.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₂
@@ -456,7 +456,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
@@ -465,7 +465,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
@@ -483,7 +483,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'']