Fix Docs

Author: Geoc2022

Game/Levels/Group/L01_MulInv.lean

@@ -7,7 +7,7 @@ Title "Right Multiplicative Inverse"
 
 namespace MyAlgebra
 
-Introduction "We will now prove that we the inverse is a also a right multiplicative inverse. This is a bit more challenging than the previous two levels, but it will be helpful to know this later on. This is one half of the \"Cancellation Rule for Groups\""
+Introduction "We will now prove that we the inverse is a also a right multiplicative inverse. This is a bit more challenging than the previous levels, but it will be helpful to know this later on. This is one half of the \"Cancellation Rule for Groups\""
 
 /--
 `mul_inv` is a proof that for all `g : G`, `g * g⁻¹ = 1` (Right Inverse Axiom).

Game/Levels/Group/L02_CancelLeft.lean

@@ -7,7 +7,7 @@ Title "Cancel Left Multiplication"
 
 namespace MyAlgebra
 
-Introduction "We now prove that we can cancel left multiplication. This is a bit more challenging than the previous two levels, but it will be helpful to know this later on. This is one half of the \"Cancellation Rule for Groups\""
+Introduction "We now prove that we can cancel left multiplication. This is a nice helper lemma to work with groups."
 
 /--
 `mul_left_cancel` is a proof that if `h * g1 = h * g2`, then `g1 = g2` - the inverse of `mul_left` is a function.

Game/Levels/Group/L03_CancelRight.lean

@@ -7,7 +7,7 @@ Title "Cancel Right Multiplication"
 
 namespace MyAlgebra
 
-Introduction "We now prove that we can cancel right multiplication - the duel of the previous level. This is the second half of the \"Cancellation Rule for Groups\""
+Introduction "We now prove that we can cancel right multiplication - the duel of the previous level."
 
 /--
 `mul_right_cancel` is a proof that if `g1 * g = g2 * g`, then `g1 = g2` - the inverse of `mul_right` is a function.