diff --git a/Test.lean b/Test.lean
index 0394cfb..5fe32cf 100644
--- a/Test.lean
+++ b/Test.lean
@@ -424,8 +424,11 @@ Unit.unit
 Nat.pow.match_1
 Nat.mul.match_1
 Nat.add.match_1
+Nat.add._f
 Nat.add
+Nat.mul._f
 Nat.mul
+Nat.pow._f
 Nat.pow
 instNatPowNat
 BitVec
@@ -468,10 +471,12 @@ List.toByteArray.match_1
 ByteArray.casesOn
 ByteArray.push.match_1
 List.concat.match_1
+List.concat._f
 List.concat
 Array.toList
 Array.push
 ByteArray.push
+List.toByteArray.loop._f
 List.toByteArray.loop
 Array.emptyWithCapacity
 Array.empty
@@ -480,9 +485,12 @@ ByteArray.empty
 List.toByteArray
 List.flatten.match_1
 List.append.match_1
+List.append._f
 List.append
+List.flatten._f
 List.flatten
 instDecidableEqList.match_1
+List.map._f
 List.map
 List.flatMap
 Char.val
@@ -506,6 +514,7 @@ Bool.false
 Bool.true
 Bool.rec
 Nat.ble.match_1
+Nat.ble._f
 Nat.ble
 DecidableEq
 Bool.casesOn
@@ -525,14 +534,17 @@ True
 True.intro
 True.rec
 Nat.beq.match_1
+Nat.beq._f
 Nat.beq
 _private.Init.Prelude.0.noConfusion_of_Nat.aux.match_1_1
+_private.Init.Prelude.0.noConfusion_of_Nat.aux._f
 _private.Init.Prelude.0.noConfusion_of_Nat.aux
 congrArg
 noConfusion_of_Nat
 Bool.ctorIdx
 _private.Init.Prelude.0.Nat.le_of_ble_eq_true.match_1_1
 _private.Init.Prelude.0.Nat.zero_le.match_1_1
+Nat.zero_le._f
 Nat.zero_le
 Nat.le.below
 Nat.le.below.refl
@@ -543,7 +555,7 @@ Nat.le.below.casesOn
 Eq.symm
 cast
 eq_of_heq
-_private.Init.Prelude.0.Nat.succ_le_succ.match_1_4
+_private.Init.Prelude.0.Nat.succ_le_succ.match_1_7
 HAdd
 HAdd.mk
 HAdd.rec
@@ -555,12 +567,15 @@ Add.add
 instHAdd
 instAddNat
 Nat.succ_le_succ
+Nat.le_of_ble_eq_true._f
 Nat.le_of_ble_eq_true
 absurd
-_private.Init.Prelude.0.Nat.ble_eq_true_of_le.match_1_4
+_private.Init.Prelude.0.Nat.ble_eq_true_of_le.match_1_7
 _private.Init.Prelude.0.Nat.ble_self_eq_true.match_1_1
+Nat.ble_self_eq_true._f
 Nat.ble_self_eq_true
 _private.Init.Prelude.0.Nat.ble_succ_eq_true.match_1_1
+Nat.ble_succ_eq_true._f
 Nat.ble_succ_eq_true
 Nat.ble_eq_true_of_le
 Nat.not_le_of_not_ble_eq_true
@@ -590,9 +605,10 @@ Sub.rec
 Sub.sub
 instHSub
 Nat.pred
+Nat.sub._f
 Nat.sub
 instSubNat
-_private.Init.Prelude.0.Nat.le_trans.match_1_6
+_private.Init.Prelude.0.Nat.le_trans.match_1_10
 Nat.le_trans
 Nat.lt_of_lt_of_le
 And.casesOn
@@ -606,6 +622,7 @@ _private.Init.Prelude.0.Nat.pred_le_pred.match_1_1
 Nat.le_succ
 Nat.pred_le_pred
 Nat.le_of_succ_le_succ
+Nat.not_succ_le_self._f
 Nat.not_succ_le_self
 Nat.lt_irrefl
 Nat.lt_succ_of_le
@@ -618,6 +635,7 @@ Nat.sub_lt
 Nat.div_rec_lemma
 Nat.le_of_lt_succ
 Nat.div_rec_fuel_lemma
+Nat.modCore.go._f
 Nat.modCore.go
 Nat.lt_add_one
 Nat.lt_succ_self
@@ -642,7 +660,9 @@ Nat.le_succ_of_le
 _private.Init.Prelude.0.Nat.lt_or_ge.match_1_1
 Nat.eq_or_lt_of_le.match_3
 Nat.eq_or_lt_of_le.match_1
+Nat.eq_or_lt_of_le._f
 Nat.eq_or_lt_of_le
+Nat.lt_or_ge._f
 Nat.lt_or_ge
 Nat.lt_of_not_le
 Nat.modCoreGo_lt
@@ -664,6 +684,7 @@ _private.Init.Prelude.0.Nat.mul_pos.match_1_1
 _private.Init.Prelude.0.Nat.add_pos_right.match_1_1
 Nat.add_pos_right
 Nat.mul_pos
+Nat.pow_pos._f
 Nat.pow_pos
 BitVec.ofNat._proof_1
 BitVec.ofNat
@@ -677,6 +698,7 @@ Div.mk
 Div.rec
 Div.div
 instHDiv
+Nat.div.go._f
 Nat.div.go
 Nat.div
 Nat.instDiv
diff --git a/lean-toolchain b/lean-toolchain
index 14791d7..2210cba 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0
+leanprover/lean4:v4.30.0-rc1