Enable explanation optimization by default

Lean/Egg/Core/Config.lean

@@ -19,7 +19,7 @@ structure Gen where
 structure Backend where
   blockInvalidMatches := true
   shiftCapturedBVars  := true -- This option implies `blockInvalidMatches`.
-  optimizeExpl        := false
+  optimizeExpl        := true
   deriving BEq
 
 inductive Debug.ExitPoint

Lean/Egg/Core/MVars.lean

@@ -71,14 +71,14 @@ def merge (vars₁ vars₂ : MVars) : MVars where
   lvl := vars₁.lvl.merge vars₂.lvl
 
 protected structure Subst.Expr where
-  fwd  : HashMap MVarId MVarId := ∅
+  fwd : HashMap MVarId MVarId := ∅
   bwd : HashMap MVarId MVarId := ∅
 
 protected abbrev Subst.Lvl := HashMap LMVarId LMVarId
 
 structure Subst where
   expr : Subst.Expr := {}
-  lvl  : Subst.Lvl := ∅
+  lvl  : Subst.Lvl  := ∅
 
 def Subst.apply (subst : Subst) (e : Expr) : Expr :=
   e.replace replaceExpr

Lean/Egg/Core/Source.lean

@@ -11,7 +11,7 @@ inductive Side where
   deriving Inhabited, BEq, Hashable
 
 def Side.description : Side → String
-  | left => "l"
+  | left  => "l"
   | right => "r"
 
 def Side.isLeft : Side → Bool
@@ -28,7 +28,6 @@ inductive Source.NatLit where
   | pow
   | div
   | mod
-
   deriving Inhabited, BEq, Hashable
 
 inductive Source where

Lean/Egg/Tests/Groups.lean

@@ -19,7 +19,7 @@ instance [Group α] : OfNat α 0 where ofNat := zero
 
 variable [Group G] {a b : G}
 
--- NOTE: Using `@add_assoc` etc, produces `.proj` expressions.
+-- Note: Using `@add_assoc` etc, produces `.proj` expressions.
 macro "group" : tactic => `(tactic|
   egg [add_assoc, zero_add, add_zero, add_left_neg, add_right_neg]
 )
@@ -30,9 +30,9 @@ theorem add_neg_cancel_left : a + (-a + b) = b := by group
 
 theorem neg_zero : -(0 : G) = 0 := by group
 
--- TODO: What is the proof of this?
 theorem neg_add : -(a + b) = -b + -a := by
-  sorry -- group
+  calc -(a + b) = -b + -a + (a + b) + -(a + b) := by group
+              _ = -b + -a                      := by group
 
 theorem inv_inv : -(-a) = a := by
   calc -(-a) = -(-a) + (-a + a) := by group