diff --git a/content/blog/functions-inductive-propositions-lean4.md b/content/blog/functions-inductive-propositions-lean4.md
index 243701b..811b7dc 100644
--- a/content/blog/functions-inductive-propositions-lean4.md
+++ b/content/blog/functions-inductive-propositions-lean4.md
@@ -152,7 +152,7 @@ Since we don't know how to show whether collatz terminates, we can't at this tim
 ```lean 
 theorem collatz_sound (n r : Nat) : (∃ t, collatz_fun n t = some r) → collatz n r := by
   intro (H: ∃ t, collatz_fun n t = some r)
-  cases' H with t H
+  obtain ⟨t, H⟩ := H
   revert H n r
   show ∀ (n r : Nat), collatz_fun n t = some r → collatz n r