From 5f0d25867e1a18e13b6a31e4439d87ec4c204714 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 25 Apr 2023 17:29:07 +0200
Subject: [PATCH] typo

---
 server/nng/NNG/Levels/Tutorial/Level_4.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/server/nng/NNG/Levels/Tutorial/Level_4.lean b/server/nng/NNG/Levels/Tutorial/Level_4.lean
index 3723f8a..ac6cca1 100644
--- a/server/nng/NNG/Levels/Tutorial/Level_4.lean
+++ b/server/nng/NNG/Levels/Tutorial/Level_4.lean
@@ -42,7 +42,7 @@ If you ever see `… + succ …` in your goal, you should be able to use
 "
 
 Statement
-"For all natural numbers $a$, we have $a + \\operatorname{succ}(0) = a$."
+"For all natural numbers $a$, we have $a + \\operatorname{succ}(0) = \\operatorname{succ}(a)$."
     (a : ℕ) : a + succ 0 = succ a := by
   Hint "You find `{a} + succ …` in the goal, so you can use `rw` and `add_succ`
   to make progress."