diff --git a/Exchangeability/Contractability.lean b/Exchangeability/Contractability.lean
index 86b2a7be..65f26108 100644
--- a/Exchangeability/Contractability.lean
+++ b/Exchangeability/Contractability.lean
@@ -467,7 +467,7 @@ theorem contractable_of_exchangeable {μ : Measure Ω} {X : ℕ → Ω → α}
     have hexch := hX n σ
 
     -- Define embedding and projection
-    let ι : Fin (m' + 1) → Fin n := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩
+    let ι : Fin (m' + 1) → Fin n := Fin.castLE hmn
     let proj : (Fin n → α) → (Fin (m' + 1) → α) := fun f i => f (ι i)
 
     have hproj_meas : Measurable proj := by
diff --git a/Exchangeability/Util/FinsetHelpers.lean b/Exchangeability/Util/FinsetHelpers.lean
index 54760461..003a68aa 100644
--- a/Exchangeability/Util/FinsetHelpers.lean
+++ b/Exchangeability/Util/FinsetHelpers.lean
@@ -29,11 +29,9 @@ The proof uses an explicit bijection between `Fin n` and the filtered set. -/
 lemma filter_val_lt_card {m n : ℕ} (h : m ≥ n) :
     (Finset.filter (fun i : Fin m => i.val < n) Finset.univ).card = n := by
   -- Establish bijection with Fin n via the natural inclusion
-  let f : Fin n → Fin m := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt h⟩
+  let f : Fin n → Fin m := Fin.castLE h
 
-  have hf_inj : Function.Injective f := by
-    intros i j hij
-    exact Fin.ext (Fin.mk.injEq _ _ _ _ ▸ hij)
+  have hf_inj : Function.Injective f := Fin.castLE_injective h
 
   have h_image : Finset.filter (fun i : Fin m => i.val < n) Finset.univ =
                  Finset.image f Finset.univ := by
@@ -41,13 +39,9 @@ lemma filter_val_lt_card {m n : ℕ} (h : m ≥ n) :
     simp only [mem_filter, mem_univ, true_and, mem_image]
     constructor
     · intro hi_lt
-      refine ⟨⟨i.val, hi_lt⟩, ?_⟩
-      simp only [f]
-    · intro ⟨j, hj_eq⟩
-      simp only [f] at hj_eq
-      calc i.val = (⟨j.val, _⟩ : Fin m).val := by rw [← hj_eq]
-        _ = j.val := rfl
-        _ < n := j.isLt
+      exact ⟨⟨i.val, hi_lt⟩, Fin.ext rfl⟩
+    · rintro ⟨j, rfl⟩
+      exact j.isLt
 
   rw [h_image, card_image_of_injective _ hf_inj]
   simp only [card_univ, Fintype.card_fin]
diff --git a/README.md b/README.md
index 70f13a99..a99d5535 100644
--- a/README.md
+++ b/README.md
@@ -48,7 +48,7 @@ We implement **all three proofs** from Kallenberg (2005) of the key implication
 
 ### Prerequisites
 
-- [Lean 4](https://leanprover.github.io/lean4/doc/setup.html) (this project uses `lean-toolchain` pinned to 4.27.0-rc1)
+- [Lean 4](https://leanprover.github.io/lean4/doc/setup.html) (see `lean-toolchain` for the pinned version)
 - [elan](https://github.com/leanprover/elan) (Lean version manager)
 
 ### Installation