more docstrings

Author: kisonecat

.i18n/en/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.7.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Wed Jun 18 11:43:39 2025\n"
+"POT-Creation-Date: Wed Jun 18 12:03:04 2025\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -62,6 +62,86 @@ msgstr ""
 msgid "This last message appears if the level is solved."
 msgstr ""
 
+#: Game.Levels.AxiomWorld.L03_Together
+msgid "Together"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L03_Together
+msgid "Let's invoke multiple axioms to prove something."
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L03_Together
+msgid "Next we'll combine multiplication and addition via distributivity."
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L04_Distributivity
+msgid "Distributivity"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L04_Distributivity
+msgid "Addition and multiplication are related via distributivity."
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L04_Distributivity
+msgid "Multiplication distributes over addition on the left"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L04_Distributivity
+msgid "Multiplication distributes over addition on the right"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L04_Distributivity
+msgid "We still need to think about 0 and 1 in rings."
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L05_Identities
+msgid "Identities"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L05_Identities
+msgid "Rings include a 0 and a 1 which are additive and multiplicative identities."
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L05_Identities
+msgid "0 is an additive identity on the right"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L05_Identities
+msgid "0 is an additive identity on the left"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L05_Identities
+msgid "1 is an multiplicative identity on the right"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L05_Identities
+msgid "1 is an multiplicative identity on the left"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L05_Identities
+msgid "We will have to learn how to combine more axioms to prove more interesting statements."
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L06_Inverses
+msgid "Inverses"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L06_Inverses
+msgid "Every element of a ring has an additive inverse."
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L06_Inverses
+msgid "exact provides a term that completes the goal"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L06_Inverses
+msgid "Every element has an additive inverse"
+msgstr ""
+
+#: Game.Levels.AxiomWorld.L06_Inverses
+msgid "We will have to learn how to combine more axioms to prove more interesting statements."
+msgstr ""
+
 #: Game.Levels.AxiomWorld
 msgid "Axiom World"
 msgstr ""

Game/Levels/AxiomWorld/L04_Distributivity.lean

@@ -1,6 +1,4 @@
 import Game.Metadata
-import Mathlib.Algebra.Ring.Defs
-import Mathlib.Tactic.Use
 
 World "AxiomWorld"
 Level 4
@@ -17,6 +15,8 @@ TheoremDoc left_distrib as "left_distrib" in "Ring"
 /-- Multiplication distributes over addition on the right -/
 TheoremDoc right_distrib as "right_distrib" in "Ring"
 
+NewTheorem left_distrib right_distrib
+
 Statement ( a b : R ) : (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
   rw [left_distrib]
   rw [right_distrib]

Game/Levels/AxiomWorld/L05_Identities.lean

@@ -19,6 +19,8 @@ TheoremDoc mul_one as "mul_one" in "Ring"
 /-- 1 is an multiplicative identity on the left -/
 TheoremDoc one_mul as "one_mul" in "Ring"
 
+NewTheorem add_zero zero_add mul_one one_mul
+
 Statement (a : R) : (1 + 1) * a = a + a := by
   rw [right_distrib]
   rw [one_mul]

Game/Levels/AxiomWorld/L06_Inverses.lean

@@ -14,11 +14,16 @@ theorem exist_add_inv (a : R) : (∃ (b : R), a + b = 0) := by
   use -a
   exact add_right_neg a
 
-NewTactic rw
+/-- exact provides a term that completes the goal -/
+TacticDoc exact
+
+NewTactic exact
 
 /-- Every element has an additive inverse -/
 TheoremDoc exist_add_inv as "exist_add_inv" in "Ring"
 
+NewTheorem exist_add_inv
+
 Statement (a : R) : ∃ b, (a + a) + b = 0 := by
   exact exist_add_inv (a+a)