From 01c62273a5c66619d6c17c43f630f8224deee04a Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Sun, 17 Mar 2024 23:47:31 -0400
Subject: [PATCH] Updates

---
 content/blog/lean4-tutorial.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/content/blog/lean4-tutorial.md b/content/blog/lean4-tutorial.md
index 8cd2de9..cb3ec57 100644
--- a/content/blog/lean4-tutorial.md
+++ b/content/blog/lean4-tutorial.md
@@ -215,7 +215,7 @@ example {p q : Prop} (H_pq : p → q) (H_pnq : p → ¬q) : ¬p := by
   exact show False from H_nq H_q
 ```
 
-### Negation Elimination
+### Double Negation Elimination
 
 One common representation of negation elimination is to remove any double negations.
 That is $\neg \neg P$ becomes $P$.
@@ -261,6 +261,8 @@ example {p: Prop} (H_nnp : ¬¬p) : p := by
     exact show p from False.elim H_false
 ```
 
+Lean has this theorem built-in with `Classical.not_not`.
+
 ## First Order
 
 Lean is also capable of reasoning over first order logic. In this section, we'll start seeing objects/terms and predicates instead of just propositions.
@@ -498,3 +500,6 @@ inductions as writing out the cases explicitly can be daunting.
 
 If you catch any mistakes in me converting this post, let me know.
 Otherwise feel free to email me if you have any questions.
+
+Lastly, I want to give my thanks to James Oswald for helping proofread
+this post and making it better.