diff --git a/Plausible/Random.lean b/Plausible/Random.lean
index de4947b..98e1a3e 100644
--- a/Plausible/Random.lean
+++ b/Plausible/Random.lean
@@ -137,7 +137,7 @@ def randBound (α : Type u) [LE α] [BoundedRandom m α] (lo hi : α) (h : lo 
 Generate a random `Fin`.
 -/
 def randFin {n : Nat} [RandomGen g] : RandGT g m (Fin n.succ) :=
-  fun ⟨g⟩ => return randNat g 0 n |>.map Fin.ofNat ULift.up
+  fun ⟨g⟩ => return randNat g 0 n |>.map (Fin.ofNat' _) ULift.up
 
 instance {n : Nat} : Random m (Fin n.succ) where
   random := randFin
diff --git a/Plausible/Sampleable.lean b/Plausible/Sampleable.lean
index f12090e..37aeef1 100644
--- a/Plausible/Sampleable.lean
+++ b/Plausible/Sampleable.lean
@@ -157,7 +157,7 @@ instance Nat.shrinkable : Shrinkable Nat where
   shrink := Nat.shrink
 
 instance Fin.shrinkable {n : Nat} : Shrinkable (Fin n.succ) where
-  shrink m := Nat.shrink m |>.map Fin.ofNat
+  shrink m := Nat.shrink m |>.map (Fin.ofNat' _)
 
 instance BitVec.shrinkable {n : Nat} : Shrinkable (BitVec n) where
   shrink m := Nat.shrink m.toNat |>.map (BitVec.ofNat n)
@@ -269,7 +269,7 @@ instance Nat.sampleableExt : SampleableExt Nat :=
 instance Fin.sampleableExt {n : Nat} : SampleableExt (Fin (n.succ)) :=
   mkSelfContained do
     let m ← choose Nat 0 (min (← getSize) n) (Nat.zero_le _)
-    return Fin.ofNat m
+    return (Fin.ofNat' _ m)
 
 instance BitVec.sampleableExt {n : Nat} : SampleableExt (BitVec n) :=
   mkSelfContained do
diff --git a/lean-toolchain b/lean-toolchain
index 3450f2d..cf25a98 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
\ No newline at end of file
+leanprover/lean4:v4.15.0-rc1