oh I'm a fool, original lemmatab was better

leanprover-community · Dec 20, 2023 · 98598bf · 98598bf
1 parent 09c16e9
commit 98598bf
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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 "Peano"
+LemmaTab "012"
 
 namespace MyNat