diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
index 20bfb663..310a4464 100644
--- a/.github/workflows/blueprint.yml
+++ b/.github/workflows/blueprint.yml
@@ -24,8 +24,18 @@ permissions:
   actions: write          # Write access to GitHub Actions
 
 env:
-  LEAN_EXPOSITION_REPO: LeanMachineLearning/exposition
-  LEAN_EXPOSITION_REF: main
+  REFEREE_REPO: LeanMachineLearning/exposition
+  # The referee release to use. Leave empty for the most recent one; set a tag (e.g. `v0.1.0`) to
+  # pin the site generator, which is worth doing once the output is being read by anyone.
+  #
+  # A *release* rather than a run artifact on purpose: release assets of a public repository need no
+  # authentication and never expire, while a cross-repository artifact download needs a PAT with
+  # `actions:read` (a workflow's own GITHUB_TOKEN cannot reach another repository's artifacts) and
+  # is deleted after 90 days.
+  REFEREE_VERSION: ""
+  # Kept as `exposition` rather than renamed to `referee` along with the tool: this path is the
+  # published URL, and existing links to it would break.
+  REFEREE_SITE_URL: https://leanmachinelearning.org/LML/exposition
 
 jobs:
   build_project:
@@ -59,29 +69,89 @@ jobs:
         run: |
           ./scripts/build_docs.sh
 
-      - name: Clone lean-exposition
+      - name: Download referee binary
         if: github.event_name == 'push'
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          git clone --depth 1 --branch "$LEAN_EXPOSITION_REF" \
-            "https://github.com/$LEAN_EXPOSITION_REPO" /tmp/lean-exposition
+          set -euo pipefail
+          mkdir -p /tmp/referee
+          gh release download ${REFEREE_VERSION:+"$REFEREE_VERSION"} \
+            -R "$REFEREE_REPO" \
+            --pattern 'referee-linux-x86_64-*.tar.gz' \
+            --dir /tmp/referee --clobber
+          tar -xzf /tmp/referee/referee-linux-x86_64-*.tar.gz -C /tmp/referee
+          referee_bin=$(echo /tmp/referee/referee-linux-x86_64-*/referee)
+          chmod +x "$referee_bin"
+          echo "REFEREE_BIN=$referee_bin" >> "$GITHUB_ENV"
 
-      - name: Build exposition binary
+          # `referee` is a Lean executable built with `supportInterpreter := true`, so it loads the
+          # shared library of the toolchain it was compiled against and has to match this project's.
+          # Checked here because the alternative is a link-time failure four steps later that says
+          # nothing about the cause.
+          want=$(tr -d '[:space:]' < lean-toolchain)
+          got=$(jq -r .lean_toolchain "$(dirname "$referee_bin")/metadata.json" | tr -d '[:space:]')
+          if [ "$want" != "$got" ]; then
+            echo "::error::referee was built for $got but this project uses $want. Publish a \
+              referee release from a matching toolchain, or pin REFEREE_VERSION to one."
+            exit 1
+          fi
+
+      # The previous run's collected data, so the site can say what changed since it. Optional in
+      # every direction: the first run has nothing to download, a failed lookup is swallowed, and
+      # `build-site` simply omits the Changes page when no baseline reaches it.
+      - name: Fetch previous referee data for the revision diff
         if: github.event_name == 'push'
+        continue-on-error: true
+        env:
+          GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
-          cd /tmp/lean-exposition && lake build exposition
-          echo "EXPOSITION_BIN=/tmp/lean-exposition/.lake/build/bin/exposition" >> "$GITHUB_ENV"
+          set -euo pipefail
+          run_id=$(gh run list -R "$GITHUB_REPOSITORY" \
+            --workflow "${{ github.workflow }}" --branch "${{ github.ref_name }}" \
+            --status success --limit 1 --json databaseId --jq '.[0].databaseId // empty')
+          [ -n "$run_id" ] || { echo "no earlier successful run; skipping the baseline"; exit 0; }
+          gh run download "$run_id" -R "$GITHUB_REPOSITORY" \
+            -n referee-data -D /tmp/referee-baseline
+          echo "REFEREE_BASELINE=/tmp/referee-baseline/referee-data.json" >> "$GITHUB_ENV"
 
-      - name: Build exposition documentation
+      - name: Build the referee site
         if: github.event_name == 'push'
         run: |
-          lake env "$EXPOSITION_BIN" \
-            --root LeanMachineLearning \
-            --repo-url https://github.com/LeanMachineLearning/LML \
-            --site-url https://leanmachinelearning.org/LML/exposition \
-            --output ./exposition \
-            --exclude-lib LMLTutorial
-          mkdir -p home_page/exposition
-          cp -r exposition/html-multi/* home_page/exposition
+          set -euo pipefail
+          # The phase split: everything needing a Lean environment produces data, and rendering is a
+          # pure function of that data. `--exclude-lib` applies to the three phases that import the
+          # project, and to none of `build-site`, which reads only the JSON. `highlight-extracted`
+          # is deliberately skipped — it re-elaborates every extracted file and costs more than the
+          # rest of this job combined; without it the standalone files are still written and linked,
+          # just not rendered inline.
+          lake env "$REFEREE_BIN" collect \
+            --root LeanMachineLearning --exclude-lib LMLTutorial --data referee-data.json
+          lake env "$REFEREE_BIN" extract \
+            --data referee-data.json --exclude-lib LMLTutorial --output ./referee-site
+          lake env "$REFEREE_BIN" highlight \
+            --data referee-data.json --output ./referee-site
+          # `--trust` is an editorial claim, not a derived fact: it says whoever publishes this site
+          # vouches for Mathlib and everything under it. Drop it and every upstream package counts
+          # as unaudited; name more packages to vouch for more.
+          "$REFEREE_BIN" build-site \
+            --data referee-data.json \
+            --output ./referee-site \
+            --repo-url "https://github.com/$GITHUB_REPOSITORY" \
+            --site-url "$REFEREE_SITE_URL" \
+            --trust mathlib \
+            ${REFEREE_BASELINE:+--baseline "$REFEREE_BASELINE"} \
+            ${REFEREE_BASELINE:+--baseline-label "the previous build"}
+
+      # Kept as an artifact so the *next* run can diff against it. Also the thing to download when
+      # you want to re-render the site locally without re-importing the project.
+      - name: Upload referee data
+        if: github.event_name == 'push'
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: referee-data
+          path: referee-data.json
+          retention-days: 90
 
       - name: Compile blueprint and documentation
         uses: leanprover-community/docgen-action@7b5b9a1822650bd45aaeb4182d94bceba2030f89 # 2026-04-14
@@ -91,6 +161,16 @@ jobs:
           build-page: false
           deploy: false
 
+      # After the docs step, which writes into the same folder alongside `tutorial/` from
+      # `build_docs.sh`. Those steps only ever add, so the order is not load-bearing — but copying
+      # last keeps the referee output out of reach of anything else that writes there.
+      - name: Add the referee site to the home page
+        if: github.event_name == 'push'
+        run: |
+          set -euo pipefail
+          mkdir -p home_page/exposition
+          cp -r referee-site/html-multi/. home_page/exposition/
+
       - name: "Upload website (API documentation, blueprint and any home page)"
         if: github.event_name == 'push'
         uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5.0.0
diff --git a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
index 7c7bf9af..01f4e195 100644
--- a/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
+++ b/LeanMachineLearning/ForMathlib/MeasureTheory/Order/MeasurableArg.lean
@@ -74,7 +74,7 @@ lemma measurable_argmax [MeasurableSpace ι] [MeasurableEq α] [MeasurableSup₂
     refine MeasurableSet.iUnion fun S ↦ (.iUnion fun hS ↦ ?_)
     exact measurableSet_eq_fun (by fun_prop) measurable_const
   ext f
-  simp only [Set.mem_setOf_eq, Set.mem_iUnion, exists_prop, exists_eq_right']
+  simp only [Set.mem_ofPred_eq, Set.mem_iUnion, exists_prop, exists_eq_right']
   constructor
   · intro hf x hx
     rw [← hf]
diff --git a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
index 9925b4e2..5b3c7a2b 100644
--- a/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/Independence/CondDistrib.lean
@@ -457,7 +457,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
       (Measure.map (fun ω ↦ (X ω, Z ω)) μ ⊗ₘ κ) (s ∩ {p | p.1.2 = b}) by
     have hs_iUnion : s = ⋃ b, s ∩ {p | p.1.2 = b} := by
       ext p
-      simp only [Set.mem_iUnion, Set.mem_inter_iff, Set.mem_setOf_eq]
+      simp only [Set.mem_iUnion, Set.mem_inter_iff, Set.mem_ofPred_eq]
       grind
     have h_disj : Pairwise (Function.onFun Disjoint fun b ↦ s ∩ {p | p.1.2 = b}) := by
       intro i j hij
@@ -486,13 +486,13 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
           ((measurableSet_singleton _).preimage (by fun_prop))
       · fun_prop
       · exact (measurableSet_singleton _).preimage (by fun_prop)
-      simp only [Set.preimage_setOf_eq]
+      simp only [Set.preimage_ofPred_eq]
       classical
       have h_le : ∫⁻ a, (κ (X a, Z a)) {a_1 | Z a = b} ∂μ ≤
           ∫⁻ a, {a' | Z a' = b}.indicator (fun _ ↦ κ.bound) a ∂μ := by
         gcongr with a
         by_cases hZ : Z a = b
-        · simp only [hZ, Set.setOf_true, Set.mem_setOf_eq, Set.indicator_of_mem]
+        · simp only [hZ, Set.ofPred_true, Set.mem_ofPred_eq, Set.indicator_of_mem]
           exact κ.measure_le_bound _ _
         · simp [hZ]
       refine le_antisymm (h_le.trans ?_) zero_le
@@ -525,8 +525,8 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
     rw [← h1, ← mul_assoc, ENNReal.mul_inv_cancel hb (by simp), one_mul]
   convert h1'
   · ext x
-    simp only [Set.preimage_inter, Set.preimage_setOf_eq, Set.mem_inter_iff, Set.mem_preimage,
-      Set.mem_setOf_eq]
+    simp only [Set.preimage_inter, Set.preimage_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage,
+      Set.mem_ofPred_eq]
     grind
   · rw [Measure.compProd_apply, Measure.compProd_apply, lintegral_map, lintegral_map]
     rotate_left
@@ -538,7 +538,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
     · exact hs'
     · exact hs.inter ((measurableSet_singleton _).preimage (by fun_prop))
     rw [lintegral_cond, ← mul_assoc, ENNReal.mul_inv_cancel hb (by simp), one_mul]
-    simp only [Set.preimage_inter, Set.preimage_setOf_eq, Kernel.coe_comap, Function.comp_apply]
+    simp only [Set.preimage_inter, Set.preimage_ofPred_eq, Kernel.coe_comap, Function.comp_apply]
     classical
     have h_eq : (fun a ↦ κ (X a, Z a) (Prod.mk (X a, Z a) ⁻¹' s ∩ {a_1 | Z a = b})) =
         {a | Z a = b}.indicator
@@ -550,7 +550,7 @@ lemma condDistrib_prod_of_forall_condDistrib_cond [Countable Ω'] [IsFiniteMeasu
     swap; · exact (measurableSet_singleton _).preimage (by fun_prop)
     refine setLIntegral_congr_fun ((measurableSet_singleton _).preimage (by fun_prop)) fun a ha ↦ ?_
     congr 1 with ω
-    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_setOf_eq, and_iff_left_iff_imp]
+    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_ofPred_eq, and_iff_left_iff_imp]
     grind
 
 lemma cond_of_indepFun [IsZeroOrProbabilityMeasure μ] (h : IndepFun X T μ)
diff --git a/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean b/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean
index 785aab28..bf8cc83d 100644
--- a/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean
+++ b/LeanMachineLearning/ForMathlib/Probability/Kernel/KernelSub.lean
@@ -149,7 +149,7 @@ lemma measurableSet_eq (κ η : Kernel α β) [IsFiniteKernel κ] [IsFiniteKerne
   classical
   have h_sub : {a | κ a = η a} = {a | (κ - η) a = 0} ∩ {a | (η - κ) a = 0} := by
     ext1 a
-    simp only [Set.mem_setOf_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]
+    simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, sub_apply_eq_zero_iff_le]
     exact ⟨fun h ↦ by simp [h], fun h ↦ le_antisymm h.1 h.2⟩
   rw [h_sub]
   refine MeasurableSet.inter ?_ ?_
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
index 530abdc2..bcba73ed 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/ETC.lean
@@ -226,7 +226,7 @@ lemma expectation_pullCount_le [Nonempty (Fin K)]
   have : (fun ω ↦ (pullCount A a n ω : ℝ))
       =ᵐ[P] fun ω ↦ m + (n - K * m) * {ω' | A (K * m) ω' = a}.indicator (fun _ ↦ 1) ω := by
     filter_upwards [pullCount_of_ge h a hm hn] with ω h
-    simp only [h, Set.indicator_apply, Set.mem_setOf_eq, mul_ite, mul_one, mul_zero, Nat.cast_add,
+    simp only [h, Set.indicator_apply, Set.mem_ofPred_eq, mul_ite, mul_one, mul_zero, Nat.cast_add,
       Nat.cast_ite, CharP.cast_eq_zero, add_right_inj]
     norm_cast
   rw [integral_congr_ae this, integral_add (integrable_const _), integral_const_mul]
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean
index 444f290d..53643f14 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/Regret/BayesRegretTS.lean
@@ -233,7 +233,7 @@ lemma integral_sum_range_actionMean_bestAction_sub_ucb_bestAction_le {alg : Algo
         intro ω hω
         apply sum_nonpos
         intro t ht
-        rw [Set.mem_compl_iff, Set.mem_setOf_eq] at hω
+        rw [Set.mem_compl_iff, Set.mem_ofPred_eq] at hω
         push Not at hω
         grind [hω t (mem_range.mp ht), ucb, actionMean]
     _ ≤ ∫ ω in F, ∑ t ∈ range n, (u - l) ∂P := by
@@ -284,7 +284,7 @@ lemma integral_sum_range_ucb_action_sub_actionMean_action_le {alg : Algorithm (F
         · apply setIntegral_mono_on (Integrable.integrableOn (by fun_prop))
             (Integrable.integrableOn (by fun_prop)) hF.compl
           intro ω hω
-          rw [Set.mem_compl_iff, Set.mem_setOf_eq] at hω
+          rw [Set.mem_compl_iff, Set.mem_ofPred_eq] at hω
           push Not at hω
           exact sum_ucb_sub_mean_le (fun a ↦ (κ (E ω, a))[id]) (hm (E ω)) hlu
             (fun t ht hpc ↦ hω t ht (A t ω) hpc)
diff --git a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
index 7bd27312..cdda9e1f 100644
--- a/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
+++ b/LeanMachineLearning/Online/Bandit/Algorithms/UCB.lean
@@ -216,7 +216,7 @@ lemma prob_ucbIndex_le [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
       1 / (n + 1) ^ (c - 1) := by
   let s : Set (ℕ × ℝ) := {(m, x) | 0 < m ∧ x / m + √(2 * (c * σ2) * log (↑n + 1) / m) ≤ (ν a)[id]}
   have hs : MeasurableSet s := by
-    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOf, s]
+    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOfPred, s]
     fun_prop
   classical
   calc P {h | 0 < pullCount A a n h ∧ empMean A R a n h + ucbWidth A (c * σ2) a n h ≤ (ν a)[id]}
@@ -234,8 +234,8 @@ lemma prob_ucbIndex_le [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
     refine Finset.sum_congr rfl fun k hk ↦ ?_
     congr with ω
     have hk : 0 < k := by grind
-    simp only [Nat.cast_nonneg, sqrt_div', id_eq, Set.preimage_setOf_eq, hk, true_and,
-      Set.mem_setOf_eq, s]
+    simp only [Nat.cast_nonneg, sqrt_div', id_eq, Set.preimage_ofPred_eq, hk, true_and,
+      Set.mem_ofPred_eq, s]
     grind
   _ ≤ ∑ k ∈ Icc 1 n, (1 : ℝ≥0∞) / (n + 1) ^ c := by
     gcongr with k hk
@@ -259,7 +259,7 @@ lemma prob_ucbIndex_ge [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
       (ν a)[id] ≤ empMean A R a n h - ucbWidth A (c * σ2) a n h} ≤ 1 / (n + 1) ^ (c - 1) := by
   let s : Set (ℕ × ℝ) := {(m, x) | 0 < m ∧ (ν a)[id] ≤ x / m - √(2 * (c * σ2) * log (↑n + 1) / m)}
   have hs : MeasurableSet s := by
-    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOf, s]
+    simp only [Nat.cast_nonneg, sqrt_div', id_eq, measurableSet_setOfPred, s]
     fun_prop
   classical
   calc P {h | 0 < pullCount A a n h ∧ (ν a)[id] ≤ empMean A R a n h - ucbWidth A (c * σ2) a n h}
@@ -277,8 +277,8 @@ lemma prob_ucbIndex_ge [Nonempty (Fin K)] {alg : Algorithm (Fin K) ℝ}
     refine Finset.sum_congr rfl fun k hk ↦ ?_
     congr with ω
     have hk : 0 < k := by grind
-    simp only [id_eq, Nat.cast_nonneg, sqrt_div', Set.preimage_setOf_eq, hk, true_and,
-      Set.mem_setOf_eq, s]
+    simp only [id_eq, Nat.cast_nonneg, sqrt_div', Set.preimage_ofPred_eq, hk, true_and,
+      Set.mem_ofPred_eq, s]
     grind
   _ ≤ ∑ k ∈ Icc 1 n, (1 : ℝ≥0∞) / (n + 1) ^ c := by
     gcongr with k hk
@@ -397,7 +397,7 @@ lemma some_sum_eq_zero [Nonempty (Fin K)]
   have h_gt := time_gt_of_pullCount_gt_one h a (ν := ν) (c := c * σ2) (hK := hK)
   filter_upwards [h_ae, h_gt] with ω h_le h_time_ge
   simp only [id_eq, tsub_le_iff_right, sum_eq_zero_iff, mem_range, Set.indicator_apply_eq_zero,
-    Set.mem_setOf_eq, Pi.one_apply, one_ne_zero, imp_false, not_and, not_le]
+    Set.mem_ofPred_eq, Pi.one_apply, one_ne_zero, imp_false, not_and, not_le]
   intro k hn h_arm hC_lt h_le_best
   by_contra! h_le_arm
   have h := pullCount_arm_le (by positivity : 0 ≤ c * σ2) h_le_best (by simpa) ?_ ?_ ?_
@@ -472,12 +472,12 @@ lemma expectation_pullCount_le'
       (measurableSet_lt (by fun_prop) (by fun_prop))
   have h_meas_1 b : Measurable fun h ↦ {s | 0 < pullCount A a s h ∧ (ν a)[id] <
       empMean A R a s h - ucbWidth A (c * σ2) a s h}.indicator (1 : ℕ → ℕ) b := by
-    simp only [id_eq, Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
+    simp only [id_eq, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply]
     exact Measurable.ite (h_set_1 _) (by fun_prop) (by fun_prop)
   have h_meas_2 b : Measurable fun h ↦ {s | 0 < pullCount A (bestArm ν) s h ∧
       empMean A R (bestArm ν) s h + ucbWidth A (c * σ2) (bestArm ν) s h <
           (ν (bestArm ν))[id]}.indicator (1 : ℕ → ℕ) b := by
-    simp only [id_eq, Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
+    simp only [id_eq, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply]
     exact Measurable.ite (h_set_2 _) (by fun_prop) (by fun_prop)
   calc ∫⁻ ω, pullCount A a n ω ∂P
   _ ≤ ∫⁻ ω, C a + 1 +
diff --git a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
index 399ec624..138f013a 100644
--- a/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
+++ b/LeanMachineLearning/Online/Bandit/ArrayProbSpace.lean
@@ -436,7 +436,7 @@ lemma stepsUntil_indicator_congr (alg : Algorithm 𝓐 R) (a : 𝓐) (m n : ℕ)
         ω =
       {ω | action alg (n + 1) ω = a ∧ pullCount (action alg) a (n + 1) ω = m}.indicator
         (fun _ ↦ 1) ω' := by
-  simp only [Set.indicator_apply, Set.mem_setOf_eq]
+  simp only [Set.indicator_apply, Set.mem_ofPred_eq]
   simp_rw [stepsUntil_congr alg a m n hω1 hω2_ne hω2_eq]
 
 end Congruence
@@ -822,12 +822,12 @@ lemma indepFun_snd_apply_aux (ν : Kernel 𝓐 R) [IsMarkovKernel ν] (a : 𝓐)
         have h_indep := indep_iSup_of_disjoint h_le h_iindep' h_disjoint
         convert h_indep using 2
         · simp only [Set.mem_singleton_iff, iSup_iSup_eq_left]
-        · simp only [ne_eq, Set.mem_setOf_eq, iSup_subtype']
+        · simp only [ne_eq, Set.mem_ofPred_eq, iSup_subtype']
       have h_proj_preimage : proj ⁻¹' t' = (fun ω₂ ↦ (rows_lt_m ω₂, other_cols ω₂)) ⁻¹'
           {p | ((fun r k ↦ if hm : m ≠ 0 then
             r ⟨min k (m - 1), Finset.mem_Iio.mpr (h_row_bound hm k)⟩
             else Nonempty.some inferInstance) p.1, p.2) ∈ t'}
-          := by ext ω₂; simp only [Set.mem_preimage, Set.mem_setOf_eq, h_proj_factor]
+          := by ext ω₂; simp only [Set.mem_preimage, Set.mem_ofPred_eq, h_proj_factor]
       rw [indepFun_iff_measure_inter_preimage_eq_mul] at h_indep_combined
       rw [h_proj_preimage]
       let T : Set ((Iio m → R) × (ℕ → {b : 𝓐 // b ≠ a} → R)) :=
@@ -920,7 +920,7 @@ lemma indepFun_snd_hist_cond [Countable 𝓐] (alg : Algorithm 𝓐 R)
     congr!
     congr with ω
     simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply,
-      Set.mem_setOf_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
+      Set.mem_ofPred_eq, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
       Classical.not_imp, Decidable.not_not, and_congr_right_iff]
     intro ha
     simp [ha]
@@ -1073,7 +1073,7 @@ lemma hasCondDistrib_reward_pullCount_action
         pullCount (action alg) a (n + 1) ω = m}).indicator 1 ⁻¹' {1}] := by
     congr with ω
     simp only [Set.mem_preimage, Set.mem_singleton_iff, Prod.mk.injEq, Set.indicator_apply,
-      Set.mem_setOf_eq, Pi.one_apply, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
+      Set.mem_ofPred_eq, Pi.one_apply, ite_eq_left_iff, not_and, zero_ne_one, imp_false,
       Classical.not_imp, Decidable.not_not, and_congr_right_iff]
     intro ha
     simp [ha]
@@ -1088,7 +1088,7 @@ lemma hasCondDistrib_reward_pullCount_action
     · rw [Measure.map_apply (by fun_prop) (by simp)] at ham
       convert ham
       ext ω
-      simp only [Set.mem_preimage, Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply,
+      simp only [Set.mem_preimage, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply,
         Set.mem_singleton_iff, ite_eq_left_iff, not_and, zero_ne_one, imp_false, Classical.not_imp,
         Decidable.not_not, Prod.mk.injEq, and_congr_right_iff]
       intro ha
@@ -1150,7 +1150,7 @@ lemma hasCondDistrib_reward_hist_action_pullCount
     · simp
     · convert ham
       ext ω
-      simp only [Set.mem_preimage, Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply,
+      simp only [Set.mem_preimage, Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply,
         Set.mem_singleton_iff, ite_eq_left_iff, not_and, zero_ne_one, imp_false, Classical.not_imp,
         Decidable.not_not, Prod.mk.injEq, and_congr_right_iff]
       intro ha
diff --git a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
index 5284ca37..77ebde03 100644
--- a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
+++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
@@ -144,7 +144,7 @@ lemma reward_cond_stepsUntil [StandardBorelSpace Ω] [Countable 𝓐]
       (fun ω ↦ R n ω.1) := by
     congr 2 with ω
     simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_singleton_iff, Set.indicator_apply,
-      Set.mem_setOf_eq, Pi.one_apply, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
+      Set.mem_ofPred_eq, Pi.one_apply, ite_eq_left_iff, zero_ne_one, imp_false, Decidable.not_not]
     rw [and_comm]
   _ = 𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1 ← a; 𝔓] := by
     rw [cond_of_condIndepFun (by fun_prop)]
diff --git a/LeanMachineLearning/Online/Bandit/SumRewards.lean b/LeanMachineLearning/Online/Bandit/SumRewards.lean
index 7eadf3c5..4d9fc081 100644
--- a/LeanMachineLearning/Online/Bandit/SumRewards.lean
+++ b/LeanMachineLearning/Online/Bandit/SumRewards.lean
@@ -50,7 +50,7 @@ lemma prob_pullCount_prod_sumRewards_mem_le (a : 𝓐) (n : ℕ)
   calc 𝔓 ((fun ω ↦ (pullCount A a n ω, ∑ i ∈ range (pullCount A a n ω), ω.2 i a)) ⁻¹' s)
   _ ≤ 𝔓 {ω | ∃ k ≤ n, (k, ∑ i ∈ range k, ω.2 i a) ∈ s} := by
     refine measure_mono fun ω hω ↦ ?_
-    simp only [Set.mem_setOf_eq] at hω ⊢
+    simp only [Set.mem_ofPred_eq] at hω ⊢
     exact ⟨pullCount A a n ω, pullCount_le _ _ _, hω⟩
   _ = 𝔓 (⋃ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s),
       {ω | (k, ∑ i ∈ range k, ω.2 i a) ∈ s}) := by congr 1; ext; simp; grind
@@ -109,14 +109,14 @@ lemma prob_sumRewards_le_sumRewards_le [Fintype 𝓐] (a : 𝓐) (n m₁ m₂ :
   _ ≤ 𝔓 ((fun ω ↦ (∑ i ∈ range m₁, ω.2 i (bestArm ν), ∑ i ∈ range m₂, ω.2 i a)) ⁻¹'
         {p | p.1 ≤ p.2}) := by
       refine measure_mono fun ω hω ↦ ?_
-      simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq] at hω ⊢
+      simp only [Set.preimage_ofPred_eq, Set.mem_ofPred_eq] at hω ⊢
       grind
   _ = streamMeasure ν
       {ω | ∑ i ∈ range m₁, ω i (bestArm ν) ≤ ∑ i ∈ range m₂, ω i a} := by
     rw [← Measure.snd_prod (μ := (Measure.infinitePi fun (_ : ℕ) ↦ (volume : Measure unitInterval)))
       (ν := streamMeasure ν), Measure.snd, Measure.map_apply (by fun_prop)]
     · rfl
-    simp only [measurableSet_setOf]
+    simp only [measurableSet_setOfPred]
     fun_prop
 
 lemma probReal_sumRewards_le_sumRewards_le [Fintype 𝓐] (a : 𝓐) (n m₁ m₂ : ℕ) :
@@ -348,7 +348,7 @@ lemma probReal_sumRewards_le_sumRewards_le [Fintype 𝓐] [MeasurableSingletonCl
   refine le_trans (le_of_eq ?_)
     (ArrayModel.probReal_sumRewards_le_sumRewards_le (alg := alg) a n m₁ m₂)
   let s := {p : ℕ × ℕ × ℝ × ℝ | p.1 = m₁ ∧ p.2.1 = m₂ ∧ p.2.2.1 ≤ p.2.2.2}
-  have hs : MeasurableSet s := by simp only [measurableSet_setOf, s]; fun_prop
+  have hs : MeasurableSet s := by simp only [measurableSet_setOfPred, s]; fun_prop
   change P.real ((fun ω ↦ (pullCount A (bestArm ν) n ω,
       pullCount A a n ω, sumRewards A R (bestArm ν) n ω, sumRewards A R a n ω)) ⁻¹' s) =
     (ArrayModel.arrayMeasure ν).real
@@ -514,7 +514,7 @@ lemma prob_sumRewards_sub_pullCount_mul_ge_le_of_Fintype [Fintype 𝓐] [Measura
     _ ≤ ∑ a, P {ω | ∃ t < n, pullCount A a t ω ≠ 0 ∧
                 √(2 * pullCount A a t ω * σ2 * Real.log (1 / δ)) ≤
                   sumRewards A R a t ω - pullCount A a t ω * (ν a)[id]} := by
-        rw [Set.setOf_exists]
+        rw [Set.ofPred_exists]
         exact measure_iUnion_fintype_le _ _
     _ ≤ ∑ a, ENNReal.ofReal ((n - 1) * δ) :=
         sum_le_sum fun a _ ↦ prob_sumRewards_sub_pullCount_mul_ge_le hσ2 (hν a) h hδ
diff --git a/LeanMachineLearning/SequentialLearning/FiniteActions.lean b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
index 4af1fb9a..f9723003 100644
--- a/LeanMachineLearning/SequentialLearning/FiniteActions.lean
+++ b/LeanMachineLearning/SequentialLearning/FiniteActions.lean
@@ -153,7 +153,7 @@ lemma pullCount_le_add (a : 𝓐) (n C : ℕ) (ω : Ω) :
         pullCount A a n ω := by
       rw [pullCount_eq_sum]
       gcongr with s hs
-      simp only [Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
+      simp only [Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply]
       grind
     induction n with
     | zero => simp
@@ -164,7 +164,7 @@ lemma pullCount_le_add (a : 𝓐) (n C : ℕ) (ω : Ω) :
           (h_le n).trans h_pc
         grw [hn']
         gcongr
-        simp only [Set.indicator_apply, Set.mem_setOf_eq, Pi.one_apply]
+        simp only [Set.indicator_apply, Set.mem_ofPred_eq, Pi.one_apply]
         grind
       · refine le_trans ?_ hn
         simp [h_pc]
@@ -283,7 +283,7 @@ lemma stepsUntil_zero_of_ne (hka : A 0 ω ≠ a) : stepsUntil A a 0 ω = 0 := by
   simp_rw [← bot_eq_zero, sInf_eq_bot, bot_eq_zero]
   intro n hn
   refine ⟨0, ?_, hn⟩
-  simp only [Set.mem_image, Set.mem_setOf_eq, Nat.cast_eq_zero, exists_eq_right, zero_add]
+  simp only [Set.mem_image, Set.mem_ofPred_eq, Nat.cast_eq_zero, exists_eq_right, zero_add]
   rw [← zero_add 1, pullCount_eq_pullCount_of_action_ne hka]
   simp
 
@@ -302,7 +302,7 @@ lemma stepsUntil_eq_dite (a : 𝓐) (m : ℕ) (ω : Ω)
   · refine le_antisymm ?_ ?_
     · refine sInf_le ?_
       simpa using Nat.find_spec h'
-    · simp only [le_sInf_iff, Set.mem_image, Set.mem_setOf_eq, forall_exists_index, and_imp,
+    · simp only [le_sInf_iff, Set.mem_image, Set.mem_ofPred_eq, forall_exists_index, and_imp,
         forall_apply_eq_imp_iff₂, Nat.cast_le, Nat.find_le_iff]
       exact fun n hn ↦ ⟨n, le_rfl, hn⟩
   · push Not at h'
@@ -318,7 +318,7 @@ lemma stepsUntil_eq_leastGE (a : 𝓐) (hm : m ≠ 0) :
   ext ω
   rw [stepsUntil_eq_dite]
   unfold leastGE hittingAfter
-  simp only [Nat.bot_eq_zero, zero_le, Set.mem_Ici, true_and, ENat.some_eq_coe]
+  simp only [Nat.bot_eq_zero, zero_le, Set.mem_Ici, true_and]
   have h_iff : (∃ s, pullCount A a (s + 1) ω = m) ↔ (∃ s, m ≤ pullCount A a (s + 1) ω) := by
     refine ⟨fun ⟨s, hs⟩ ↦ ⟨s, hs.ge⟩, fun ⟨s, hs⟩ ↦ ?_⟩
     exact exists_pullCount_eq_of_le hs hm
@@ -326,7 +326,7 @@ lemma stepsUntil_eq_leastGE (a : 𝓐) (hm : m ≠ 0) :
   swap; · simp_rw [h_iff]; simp [h_exists]
   rw [if_pos h_exists, dif_pos]
   swap; · rwa [h_iff]
-  norm_cast
+  simp only [ENat.some_eq_natCast, Nat.cast_inj]
   rw [Nat.find_eq_iff]
   constructor
   · apply le_antisymm
@@ -386,7 +386,7 @@ lemma stepsUntil_eq_zero_iff :
 lemma action_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
     A (stepsUntil A a m ω).toNat ω = a := by
   classical
-  simp only [stepsUntil_eq_dite, h_exists, ↓reduceDIte, ENat.toNat_coe]
+  simp only [stepsUntil_eq_dite, h_exists, ↓reduceDIte, ENat.toNat_natCast]
   have h_spec := Nat.find_spec h_exists
   have h_spec' n := Nat.find_min h_exists (m := n)
   by_cases h_zero : Nat.find h_exists = 0
@@ -418,7 +418,7 @@ lemma pullCount_stepsUntil_add_one (h_exists : ∃ s, pullCount A a (s + 1) ω =
   have h' := Nat.find_spec h_exists
   rw [h_eq]
   rw [ENat.toNat_add (by simp) (by simp)]
-  simp only [ENat.toNat_coe, ENat.toNat_one]
+  simp only [ENat.toNat_natCast, ENat.toNat_one]
   exact h'
 
 lemma pullCount_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount A a (s + 1) ω = m) :
@@ -439,7 +439,7 @@ lemma pullCount_lt_of_le_stepsUntil (a : 𝓐) {n m : ℕ} (ω : Ω)
   classical
   have h_eq := stepsUntil_eq_dite (A := A) a m ω
   simp only [h_exists, ↓reduceDIte] at h_eq
-  rw [← ENat.coe_toNat (stepsUntil_ne_top h_exists)] at hn
+  rw [← ENat.natCast_toNat (stepsUntil_ne_top h_exists)] at hn
   refine lt_of_le_of_ne ?_ ?_
   · calc pullCount A a (n + 1) ω
     _ ≤ pullCount A a (stepsUntil A a m ω + 1).toNat ω := by
@@ -450,7 +450,7 @@ lemma pullCount_lt_of_le_stepsUntil (a : 𝓐) {n m : ℕ} (ω : Ω)
     _ = m := pullCount_stepsUntil_add_one h_exists
   · refine Nat.find_min h_exists (m := n) ?_
     suffices n < (stepsUntil A a m ω).toNat by
-      rwa [h_eq, ENat.toNat_coe] at this
+      rwa [h_eq, ENat.toNat_natCast] at this
     exact mod_cast hn
 
 lemma pullCount_eq_of_stepsUntil_eq_coe {ω : Ω} (hm : m ≠ 0)
@@ -548,7 +548,7 @@ lemma measurable_stepsUntil [MeasurableSingletonClass 𝓐]
           ∃ s, pullCount A a (s + 1) k' = m} | pullCount A a (k + 1) (x : Ω) = m}
         = {x : Ω | pullCount A a (k + 1) x = m} := by
       ext x
-      simp only [Set.mem_setOf_eq, Set.coe_setOf, Set.mem_image, Subtype.exists, exists_and_left,
+      simp only [Set.mem_ofPred_eq, Set.coe_ofPred, Set.mem_image, Subtype.exists, exists_and_left,
         exists_prop, exists_eq_right_right, and_iff_left_iff_imp]
       exact fun h ↦ ⟨_, h⟩
     refine (MeasurableEmbedding.subtype_coe h_meas_set).measurableSet_image.mp ?_
@@ -580,7 +580,7 @@ lemma measurable_comap_indicator_stepsUntil_eq [MeasurableSingletonClass 𝓐]
         ext ω
         by_cases ha : A 0 ω = a
         · simp [stepsUntil_zero_of_eq ha]
-        · simp only [Set.mem_setOf_eq, stepsUntil_zero_of_ne ha, Set.mem_empty_iff_false,
+        · simp only [Set.mem_ofPred_eq, stepsUntil_zero_of_ne ha, Set.mem_empty_iff_false,
             iff_false]
           norm_cast
           exact Ne.symm hn
@@ -683,7 +683,7 @@ lemma rewardByCount_eq_add [AddMonoid R] (a : 𝓐) (m : ℕ) :
           (fun ω ↦ R' (stepsUntil A a m ω.1).toNat ω.1)
         + {ω | stepsUntil A a m ω.1 = ⊤}.indicator (fun ω ↦ ω.2 m a) := by
   ext ω
-  simp only [rewardByCount_eq_ite, ne_eq, Pi.add_apply, Set.indicator_apply, Set.mem_setOf_eq,
+  simp only [rewardByCount_eq_ite, ne_eq, Pi.add_apply, Set.indicator_apply, Set.mem_ofPred_eq,
     ite_not]
   grind
 
@@ -991,11 +991,11 @@ lemma _root_.MeasureTheory.StronglyMeasurable.div₀' {𝓐 β : Type*}
   refine ⟨fun n => hf.approx n / (hg.approx n).restrict {x | g x ≠ 0}, fun x => ?_⟩
   have : MeasurableSet {x | g x ≠ 0} := ((MeasurableSet.singleton 0).preimage hg.measurable).compl
   by_cases h : g x = 0
-  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_setOf_eq,
+  · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict, Pi.div_apply, mem_ofPred_eq,
       not_true_eq_false, not_false_eq_true, indicator_of_notMem, _root_.div_zero]
     exact tendsto_const_nhds
   · simp_all only [ne_eq, SimpleFunc.coe_div, SimpleFunc.coe_restrict,
-      Pi.div_apply, mem_setOf_eq, not_false_eq_true, indicator_of_mem]
+      Pi.div_apply, mem_ofPred_eq, not_false_eq_true, indicator_of_mem]
     exact (hf.tendsto_approx x).div (hg.tendsto_approx x) h
 
 end CopiedFromPR