enable ac_rfl

Game/Levels/Addition/Level_2.lean

@@ -53,5 +53,8 @@ $ (a + b) + c = a + (b + c). $"
   rw [hc]
   rfl
 
+-- Adding this instance to make `ac_rfl` work.
+instance : Lean.IsAssociative (α := ℕ) (·+·) := ⟨MyNat.add_assoc⟩
+
 NewLemma MyNat.zero_add
 LemmaTab "Add"

Game/Levels/Addition/Level_4.lean

@@ -39,6 +39,9 @@ $a + b = b + a$."
     rw [succ_add]
     rfl
 
+-- Adding this instance to make `ac_rfl` work.
+instance : Lean.IsCommutative (α := ℕ) (·+·) := ⟨MyNat.add_comm⟩
+
 LemmaTab "Add"
 
 Conclusion

Game/Levels/Addition/Level_6.lean

@@ -56,6 +56,8 @@ $a + b + c = a + c + b$."
   additions like this: `rw [add_comm a]` will swap around
   additions of the form `a + _`, and `rw [add_comm a b]` will only
   swap additions of the form `a + b`."
+  Branch
+    ac_rfl
   Branch
     rw [add_comm]
     Hint "`rw [add_comm]` just rewrites to first instance of `_ + _` it finds, which

Game/Tactic/ACRfl.lean

@@ -0,0 +1,16 @@
+
+import Lean
+
+-- Note: to get `ac_rfl` working (which is in core), we just
+-- need the two instances below in the files where
+-- `add_assoc` and `add_comm` are proven.
+-- This file is only for demonstration purpose.
+
+import Game.Levels.Addition.Level_2 -- defines `MyNat.add_assoc`
+import Game.Levels.Addition.Level_4 -- defines `MyNat.add_comm`
+
+instance : Lean.IsAssociative (α := ℕ) (·+·) := ⟨MyNat.add_assoc⟩
+instance : Lean.IsCommutative (α := ℕ) (·+·) := ⟨MyNat.add_comm⟩
+
+example (a b c : ℕ) : c + (b + a) = (a + b) + c := by
+  ac_rfl

Game/Tactic/Rfl.lean

@@ -16,7 +16,7 @@ open Lean Meta Elab Tactic
 
 `rfl` closes goals of the form `A = A`.
 
-Note that teh version for this game is somewhat weaker than the real one. -/
+Note that the version for this game is somewhat weaker than the real one. -/
 syntax (name := rfl) "rfl" : tactic
 
 @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>