diff --git a/HumanEvalLean/Common/Brackets.lean b/HumanEvalLean/Common/Brackets.lean
index f8f418c..28ec19c 100644
--- a/HumanEvalLean/Common/Brackets.lean
+++ b/HumanEvalLean/Common/Brackets.lean
@@ -262,7 +262,7 @@ theorem isBalanced_eq_true_iff {openBracket closeBracket : Char} {s : String} (h
   generalize hwp : isBalanced openBracket closeBracket s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case inv =>
+  case inv1 =>
     exact Std.Do.StringInvariant.withEarlyReturn
       (fun pos depth => ⌜∀ t₁ t₂, pos.Splits t₁ t₂ → minBalance (parens openBracket closeBracket t₁) = 0 ∧ depth = balance (parens openBracket closeBracket t₁)⌝)
       (fun res depth => ⌜res = false ∧ ¬ IsBalanced (parens openBracket closeBracket s)⌝)
diff --git a/HumanEvalLean/HumanEval1.lean b/HumanEvalLean/HumanEval1.lean
index 0490295..4486d48 100644
--- a/HumanEvalLean/HumanEval1.lean
+++ b/HumanEvalLean/HumanEval1.lean
@@ -53,7 +53,7 @@ theorem goal {s : String} {hbal : IsBalanced (parens '(' ')' s)} :
   generalize hwp : separateParenGroups s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case vc1.inv => exact ⇓⟨pos, ⟨curr, depth, result⟩⟩ =>
+  case inv1 => exact ⇓⟨pos, ⟨curr, depth, result⟩⟩ =>
     ⌜∀ t₁ t₂, pos.Splits t₁ t₂ →
       result.toList.flatMap (parens '(' ')') ++ (parens '(' ')' curr) = parens '(' ')' t₁ ∧
       result.toList.flatMap String.toList ++ curr.toList = t₁.toList.filter (fun c => c = '(' ∨ c = ')') ∧
diff --git a/HumanEvalLean/HumanEval119.lean b/HumanEvalLean/HumanEval119.lean
index 4c7ad0e..fa6f79d 100644
--- a/HumanEvalLean/HumanEval119.lean
+++ b/HumanEvalLean/HumanEval119.lean
@@ -41,7 +41,7 @@ theorem computeBalance_eq {s : String.Slice} :
   generalize hwp : computeBalance s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case inv => exact (⇓(pos, ⟨bal, minBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
+  case inv1 => exact (⇓(pos, ⟨bal, minBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
     bal = balance (parens '(' ')' t₁) ∧ minBal = minBalance (parens '(' ')' t₁)⌝)
   next pos _ hp bal minBal h newBal newMinBal ih =>
     simp only [↓Char.isValue, SPred.down_pure] at ⊢ ih
diff --git a/HumanEvalLean/HumanEval128.lean b/HumanEvalLean/HumanEval128.lean
index f8ec527..6bf2dfd 100644
--- a/HumanEvalLean/HumanEval128.lean
+++ b/HumanEvalLean/HumanEval128.lean
@@ -41,12 +41,7 @@ theorem List.product_eq_zero_iff {xs : List Int} :
 
 theorem Option.of_wp {α} {prog : Option α} (P : Option α → Prop) :
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P prog := by
-  intro hspec
-  simp only [wp, PredTrans.apply_pushOption, PredTrans.apply_Pure_pure, SPred.entails_nil,
-    SPred.down_pure, forall_const] at hspec
-  split at hspec
-  case h_1 a s' heq => rw [← heq] at hspec; exact hspec
-  case h_2 s' heq => rw [← heq] at hspec; exact hspec
+  cases prog <;> simp [wp, Option.instWP._aux_1, OptionT.run]
 
 theorem Option.of_wp_eq {α : Type} {x : Option α} {prog : Option α} (h : prog = x) (P : Option α → Prop) :
     (⊢ₛ wp⟦prog⟧ post⟨fun a => ⌜P (some a)⌝, fun _ => ⌜P none⌝⟩) → P x := by
diff --git a/HumanEvalLean/HumanEval129.lean b/HumanEvalLean/HumanEval129.lean
index 67f1958..3bb229f 100644
--- a/HumanEvalLean/HumanEval129.lean
+++ b/HumanEvalLean/HumanEval129.lean
@@ -2,6 +2,7 @@ module
 
 import Std
 import all Init.Data.Range.Polymorphic.RangeIterator
+public meta import Std.Tactic.Do.Syntax
 open Std Std.Do
 
 set_option mvcgen.warning false
diff --git a/HumanEvalLean/HumanEval6.lean b/HumanEvalLean/HumanEval6.lean
index d211ff9..bba1ffd 100644
--- a/HumanEvalLean/HumanEval6.lean
+++ b/HumanEvalLean/HumanEval6.lean
@@ -30,7 +30,7 @@ theorem computeMaxDepth_eq {s : String.Slice} :
   generalize hwp : computeMaxDepth s = w
   apply Std.Do.Id.of_wp_run_eq hwp
   mvcgen
-  case inv => exact (⇓(pos, ⟨bal, maxBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
+  case inv1 => exact (⇓(pos, ⟨bal, maxBal⟩) => ⌜∀ (t₁ t₂ : String), pos.Splits t₁ t₂ →
     bal = balance (parens '(' ')' t₁) ∧ maxBal = maxBalance (parens '(' ')' t₁)⌝)
   next pos _ hp bal minBal h newBal newMinBal ih =>
     simp only [↓Char.isValue, SPred.down_pure] at ⊢ ih
diff --git a/lean-toolchain b/lean-toolchain
index a07c58f..f0e2d9e 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2026-03-09
+leanprover/lean4:nightly-2026-03-22