From 09c16e9f2a886769098374878b16b9796ef93b66 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Wed, 20 Dec 2023 13:37:34 +0000
Subject: [PATCH] more appropriate lemma tab for implication L10

---
 Game/Levels/Implication/L10one_ne_zero.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Game/Levels/Implication/L10one_ne_zero.lean b/Game/Levels/Implication/L10one_ne_zero.lean
index 5464f1f..0cb7155 100644
--- a/Game/Levels/Implication/L10one_ne_zero.lean
+++ b/Game/Levels/Implication/L10one_ne_zero.lean
@@ -3,7 +3,7 @@ World "Implication"
 Level 10
 Title "1 ≠ 0"
 
-LemmaTab "012"
+LemmaTab "Peano"
 
 namespace MyNat