Resolve two test TODOs

Lean/Egg/Tests/Classes.lean

@@ -1,9 +1,8 @@
 import Egg
 
--- TODO: What is this testing?
+-- This tests how type class arguments are encoded in rewrites and matched against expressions.
 
 variable (thm : {α : Type _} → [Add α] → (a b : α) → a + b = b + a)
 
--- TODO: It feels like this is related to universe levels.
 example {a b : Nat} : a + b = b + a := by
-  sorry -- egg [thm]
+  egg [thm]

Lean/Egg/Tests/Freshman.lean

@@ -58,4 +58,4 @@ theorem freshmans_dream₃ : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3
    _ = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3           := by char_two_ring
 
 theorem freshmans_dream₃' : (x + y) ^ 3 = x ^ 3 + x * y ^ 2 + x ^ 2 * y + y ^ 3 := by
-    char_two_ring
+  char_two_ring

Lean/Egg/Tests/From.lean

@@ -12,9 +12,8 @@ example (a b : Nat) (h : a = b) : a = b := by
 example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by
   egg [h₂] from h₁
 
--- TODO: Removing the last `p` in the goal causes 'maximum recursion depth has been reached'.
-example (h : p ∧ q ∧ r) (assoc : ∀ a b c, (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)) (idem : ∀ a, a ↔ a ∧ a) :
-    r ∧ r ∧ q ∧ p ∧ q ∧ r ∧ p := by
+variable (assoc : ∀ a b c, (a ∧ b) ∧ c ↔ a ∧ (b ∧ c)) (idem : ∀ a, a ↔ a ∧ a) in
+example (h : p ∧ q ∧ r) : r ∧ r ∧ q ∧ p ∧ q ∧ r ∧ p := by
   egg [And.comm, assoc, idem] from h
 
 example (P : Nat → Prop) (hp : P Nat.zero.succ) (h : ∀ n, P n ↔ P n.succ) :