From 597fab929b87f83befae849e90de3c5eb422fa4a Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 16 Apr 2024 22:02:34 -0400 Subject: [PATCH] Small proof change --- content/blog/functions-inductive-propositions-lean4.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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