diff --git a/Lean/Egg/Tests/EndOfInput 2.lean b/Lean/Egg/Tests/EndOfInput 2.lean
index cf8fffe..ddfed78 100644
--- a/Lean/Egg/Tests/EndOfInput 2.lean	
+++ b/Lean/Egg/Tests/EndOfInput 2.lean	
@@ -4,4 +4,4 @@ import Egg
 -- "Unexpected end of input".
 
 example : 0 = 0 := by
-  egg (config := { optimizeExpl := true })
+  egg (config := { })
diff --git a/Lean/Egg/Tests/EraseForallDomains.lean b/Lean/Egg/Tests/EraseForallDomains.lean
index a057058..dd02efb 100644
--- a/Lean/Egg/Tests/EraseForallDomains.lean
+++ b/Lean/Egg/Tests/EraseForallDomains.lean
@@ -1,15 +1,16 @@
 import Egg
 
-set_option egg.eraseForallDomains true
-
+set_option egg.eraseForallDomains false in
 example (h : ∀ x y : Nat, x = y ↔ y = x) : (∀ x y : Nat, x = y) ↔ (∀ a b : Nat, b = a + 0) := by
-  egg (config := { eraseForallDomains := false }) [h, Nat.add_zero]
+  egg [h, Nat.add_zero]
 
+set_option egg.eraseForallDomains true in
 example (h : ∀ x y : Nat, x = y ↔ y = x) : (∀ x y : Nat, x = y) ↔ (∀ a b : Nat, b = a + 0) := by
   egg [h, Nat.add_zero]
 
--- BUG: the rewrite is actually bidirectional, but the domain is the only reference to the mvar for
---      `α` on the rhs.
+-- BUG: The rewrite is actually bidirectional, but the domain is the only reference to the mvar for
+--      `α` on the rhs. You can only see this in `trace.egg.encoded`, not `trace.egg.rewrites`.
 variable (h : ∀ (α : Type), (α = α) ↔ (∀ (_ : α), 0 = 0))
+set_option egg.eraseForallDomains true in
 example : True = True := by
   sorry -- egg [h]
diff --git a/Lean/Egg/Tests/EraseLambdaDomains.lean b/Lean/Egg/Tests/EraseLambdaDomains.lean
index aff3f5c..855c791 100644
--- a/Lean/Egg/Tests/EraseLambdaDomains.lean
+++ b/Lean/Egg/Tests/EraseLambdaDomains.lean
@@ -2,19 +2,21 @@ import Egg
 
 set_option egg.eraseLambdaDomains true
 
+set_option egg.eraseLambdaDomains false in
 example : (fun x => x) = (fun x => 0 + 0 + x) := by
-  egg (config := { eraseLambdaDomains := false }) [Nat.zero_add]
+  egg [Nat.zero_add]
 
 example : (fun x => x) = (fun x => 0 + 0 + x) := by
   egg [Nat.zero_add]
 
+set_option egg.eraseLambdaDomains false in
 example : (fun x => x) = (fun x => 0 + x) := by
-  egg (config := { eraseLambdaDomains := false }) [Nat.zero_add]
+  egg [Nat.zero_add]
 
 example : (fun x => x) = (fun x => 0 + x) := by
   egg [Nat.zero_add]
 
--- BUG: the rewrite is actually bidirectional, but the domain is the only reference to the mvar for
+-- BUG: The rewrite is actually bidirectional, but the domain is the only reference to the mvar for
 --      `α` on the rhs.
 variable (h : ∀ α : Type, (fun (_ : List α) => 0) = (fun _ => ([] : List α).length))
 example : True = True := by
diff --git a/Lean/Egg/Tests/EraseProofs.lean b/Lean/Egg/Tests/EraseProofs.lean
index 2eb4255..2bbc3b1 100644
--- a/Lean/Egg/Tests/EraseProofs.lean
+++ b/Lean/Egg/Tests/EraseProofs.lean
@@ -4,9 +4,10 @@ import Egg
 
 set_option egg.eraseProofs true
 
+set_option egg.eraseProofs false in
 example (i : Nat) (h : i < 10) : (Fin.mk i h).val = i := by
   have : ∀ n m (g : n < m), (Fin.mk n g).val = n := by simp
-  egg (config := { eraseProofs := false }) [this]
+  egg [this]
 
 example (i : Nat) (h : i < 10) : (Fin.mk i h).val = i := by
   have : ∀ n m (g : n < m), (Fin.mk n g).val = n := by simp
@@ -16,7 +17,7 @@ example (i : Nat) (h : ∀ i : Nat, i < 10) : (Fin.mk i (h i)).val = i := by
   have : ∀ n m (g : n < m), (Fin.mk n g).val = n := by simp
   egg [this]
 
--- BUG: the rewrite is actually bidirectional, but the proof is the only reference to the mvar for
+-- BUG: The rewrite is actually bidirectional, but the proof is the only reference to the mvar for
 --      `x` on the rhs.
 variable (h : ∀ x : Nat, x = (Exists.intro x x.zero_le).choose)
 example : True = True := by
diff --git a/Lean/Egg/Tests/Eta.lean b/Lean/Egg/Tests/Eta.lean
index 59c36cb..a8e11b4 100644
--- a/Lean/Egg/Tests/Eta.lean
+++ b/Lean/Egg/Tests/Eta.lean
@@ -4,8 +4,9 @@ import Egg
 set_option egg.genEtaRw true
 set_option egg.genBetaRw false
 
+set_option egg.genEtaRw false in
 example : (fun x => Nat.succ x) = Nat.succ := by
-  fail_if_success egg (config := { genEtaRw := false })
+  fail_if_success egg
   rfl
 
 example : (fun x => Nat.succ x) = Nat.succ := by
@@ -42,8 +43,9 @@ example : id (eta 2 Nat.succ Nat) = id Nat.succ := by
 example : (eta 10 Nat.succ Nat) = Nat.succ := by
   egg
 
+set_option egg.genEtaRw false in
 example (a : Nat) (h : ∀ b : Nat, b.succ.add a = 0) : (10 |> fun x => Nat.succ x).add a = 0 := by
-  fail_if_success egg (config := { genEtaRw := false }) [h]
+  fail_if_success egg [h]
   apply h
 
 example (a : Nat) (h : ∀ b : Nat, b.succ.add a = 0) : (10 |> fun x => Nat.succ x).add a = 0 := by
@@ -53,7 +55,7 @@ example (a : Nat) (h : ∀ b : Nat, b.succ.add a = 0) : (10 |> fun x => Nat.succ
 example : (fun x => x) = Add.add 0 := by
   sorry -- egg [Nat.zero_add]
 
-/- BUG: Why is proof reconstruction failing here? The explanation seems totally fine:
+/- TODO: Why is proof reconstruction failing here? The explanation seems totally fine:
 
   (app (app (λ (const Nat) (app f (bvar 0))) y) y)
   (app (app (Rewrite=> ≡η f) y) y)
@@ -65,8 +67,6 @@ Even stranger, if you flip the LHS and RHS of the goal, it suddenly works. The p
 in that case is the same just backwards. So a hacky fix would be to always obtain explanations from
 egg in both directions and if one fails try the other.
 -/
-set_option trace.egg true in
-set_option egg.optimizeExpl true in
 example (f i : Nat → Nat → Nat) (h₁ : f y = g) (h₂ : g y = i y (nat_lit 0)) :
     (f ·) y y = (i ·) y (nat_lit 0) := by
   sorry -- egg [h₁, h₂]
diff --git a/Lean/Egg/Tests/Groups.lean b/Lean/Egg/Tests/Groups.lean
index 5d12b14..ce4b9bb 100644
--- a/Lean/Egg/Tests/Groups.lean
+++ b/Lean/Egg/Tests/Groups.lean
@@ -34,6 +34,5 @@ theorem inv_inv : -(-a) = a := by
 theorem neg_add' : -(a + b) = -b + -a := by
   group using -a + (a + b) + -(a + b)
 
--- BUG: Try adding a hypothesis. This should cause the backend to crash.
 theorem inv_inv' : -(-a) = a := by
   group using -a + a