diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index 7369f4cb6..03271ba20 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -580,3 +580,30 @@ definition group_of_add_group (A : Type) [G : add_group A] : group A :=
   mul_left_inv    := add.left_inv⦄
 
 end algebra
+
+namespace simplifier
+
+namespace unit
+attribute algebra.zero_add [simp]
+attribute algebra.add_zero [simp]
+
+attribute algebra.one_mul [simp]
+attribute algebra.mul_one [simp]
+end unit
+
+namespace neg
+attribute algebra.neg_neg [simp]
+attribute algebra.sub_eq_add_neg [simp]
+end neg
+
+namespace ac
+attribute algebra.add.assoc [simp]
+attribute algebra.add.comm [simp]
+attribute algebra.add.left_comm [simp]
+
+attribute algebra.mul.left_comm [simp]
+attribute algebra.mul.comm [simp]
+attribute algebra.mul.assoc [simp]
+end ac
+
+end simplifier
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index a1fec765a..80a157b0a 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -195,6 +195,9 @@ section
        rewrite [-left_distrib, add.right_inv, mul_zero]
      end
 
+  theorem neg_mul_eq_neg_mul_symm : - a * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul
+  theorem neg_mul_eq_mul_neg_symm : a * - b = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg
+
   theorem neg_mul_neg : -a * -b = a * b :=
   calc
      -a * -b = -(a * -b) : by rewrite -neg_mul_eq_neg_mul
@@ -402,3 +405,22 @@ section
 end
 
 end algebra
+
+namespace simplifier
+
+namespace unit
+attribute algebra.zero_mul [simp]
+attribute algebra.mul_zero [simp]
+end unit
+
+namespace neg
+attribute algebra.neg_mul_eq_neg_mul_symm [simp]
+attribute algebra.neg_mul_eq_mul_neg_symm [simp]
+end neg
+
+namespace distrib
+attribute algebra.left_distrib [simp]
+attribute algebra.right_distrib [simp]
+end distrib
+
+end simplifier
diff --git a/library/algebra/simplifier.lean b/library/algebra/simplifier.lean
deleted file mode 100644
index e76698252..000000000
--- a/library/algebra/simplifier.lean
+++ /dev/null
@@ -1,123 +0,0 @@
-/-
-Copyright (c) 2015 Daniel Selsam. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Daniel Selsam
--/
-import algebra.ring algebra.numeral
-
-namespace simplifier
-
-namespace empty
-end empty
-
-namespace iff
-attribute eq_self_iff_true [simp]
-end iff
-
--- TODO(dhs): make these [simp] rules in the global namespace
-namespace neg_helper
-    open algebra
-    variables {A : Type} [s : ring A] (a b : A)
-    include s
-    lemma neg_mul1 : (- a) * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul
-    lemma neg_mul2 : a * (- b) = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg
-    lemma sub_def : a - b = a + (- b) := rfl
-end neg_helper
-
-namespace neg
-attribute neg_helper.neg_mul1 [simp]
-attribute neg_helper.neg_mul2 [simp]
-attribute neg_helper.sub_def [simp]
-attribute algebra.neg_neg [simp]
-end neg
-
-namespace unit
-attribute algebra.zero_add [simp]
-attribute algebra.add_zero [simp]
-
-attribute algebra.zero_mul [simp]
-attribute algebra.mul_zero [simp]
-
-attribute algebra.one_mul [simp]
-attribute algebra.mul_one [simp]
-end unit
-
-namespace ac
-export simplifier.iff simplifier.neg simplifier.unit
-
-attribute algebra.add.assoc [simp]
-attribute algebra.add.comm [simp]
-attribute algebra.add.left_comm [simp]
-
-attribute algebra.mul.left_comm [simp]
-attribute algebra.mul.comm [simp]
-attribute algebra.mul.assoc [simp]
-
-end ac
-
-namespace distrib
-attribute algebra.left_distrib [simp]
-attribute algebra.right_distrib [simp]
-end distrib
-
-namespace som
-export simplifier.ac simplifier.distrib
-end som
-
-namespace numeral
-
--- TODO(dhs): remove `add1` from the original lemmas and delete this
-namespace numeral_helper
-open algebra
-
-theorem bit1_add_bit1 {A : Type} [s : add_comm_semigroup A]
-  [s' : has_one A] (a b : A) : bit1 a + bit1 b = bit0 ((a + b) + 1)
-  := norm_num.bit1_add_bit1 a b
-
-theorem bit1_add_one {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
-  : bit1 a + one = bit0 (a + 1) := norm_num.add1_bit1 a
-
-theorem one_add_bit1 {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
-  : one + bit1 a = bit0 (a + 1) := by rewrite [!add.comm, bit1_add_one]
-
-lemma one_add_bit0 [simp] {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
-  : 1 + bit0 a = bit1 a := norm_num.one_add_bit0 a
-
-lemma bit0_add_one [simp] {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
-  : bit0 a + 1 = bit1 a := norm_num.bit0_add_one a
-
-lemma mul_bit0_helper0 [simp] {A : Type} [s : comm_ring A] (a b : A)
-  : bit0 a * bit0 b = bit0 (bit0 a * b) := norm_num.mul_bit0_helper (bit0 a) b (bit0 a * b) rfl
-
-lemma mul_bit0_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A)
-  : bit1 a * bit0 b = bit0 (bit1 a * b) := norm_num.mul_bit0_helper (bit1 a) b (bit1 a * b) rfl
-
-lemma mul_bit1_helper0 [simp] {A : Type} [s : comm_ring A] (a b : A)
-  : bit0 a * bit1 b = bit0 (bit0 a * b) + bit0 a := norm_num.mul_bit1_helper (bit0 a) b (bit0 a * b) (bit0 (bit0 a * b) + bit0 a) rfl rfl
-
-lemma mul_bit1_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A)
-  : bit1 a * bit1 b = bit0 (bit1 a * b) + bit1 a := norm_num.mul_bit1_helper (bit1 a) b (bit1 a * b) (bit0 (bit1 a * b) + bit1 a) rfl rfl
-
-end numeral_helper
-
-export simplifier.ac
-
-attribute norm_num.bit0_add_bit0 [simp]
-attribute numeral_helper.bit1_add_one [simp]
-attribute norm_num.bit1_add_bit0 [simp]
-attribute numeral_helper.bit1_add_bit1 [simp]
-attribute norm_num.bit0_add_bit1 [simp]
-attribute numeral_helper.one_add_bit1 [simp]
-
-attribute norm_num.one_add_one [simp]
-attribute numeral_helper.one_add_bit0 [simp]
-attribute numeral_helper.bit0_add_one [simp]
-
-attribute numeral_helper.mul_bit0_helper0 [simp]
-attribute numeral_helper.mul_bit0_helper1 [simp]
-attribute numeral_helper.mul_bit1_helper0 [simp]
-attribute numeral_helper.mul_bit1_helper1 [simp]
-
-end numeral
-
-end simplifier
diff --git a/library/init/simplifier.lean b/library/init/simplifier.lean
index 10c7e65ca..de6804522 100644
--- a/library/init/simplifier.lean
+++ b/library/init/simplifier.lean
@@ -8,6 +8,13 @@ import init.logic
 
 namespace simplifier
 
+namespace empty
+end empty
+
+namespace prove
+attribute eq_self_iff_true [simp]
+end prove
+
 namespace unit_simp
 open eq.ops
 
diff --git a/src/library/blast/simplifier/simp_rule_set.cpp b/src/library/blast/simplifier/simp_rule_set.cpp
index 9410afef3..e2f4e5d33 100644
--- a/src/library/blast/simplifier/simp_rule_set.cpp
+++ b/src/library/blast/simplifier/simp_rule_set.cpp
@@ -556,6 +556,20 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios,
     return set;
 }
 
+simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, std::initializer_list<name> const & nss) {
+    simp_rule_sets set;
+    for (name const & ns : nss) {
+        list<rrs_entry> const * entries = rrs_ext::get_entries(env, ns);
+        if (entries) {
+            for (auto const & e : *entries) {
+                tmp_type_context tctx(env, ios);
+                set = add_core(tctx, set, e.m_name, e.m_priority);
+            }
+        }
+    }
+    return set;
+}
+
 io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s) {
     options const & opts = out.get_options();
     out.get_stream() << mk_pair(s.pp(out.get_formatter()), opts);
diff --git a/src/library/blast/simplifier/simp_rule_set.h b/src/library/blast/simplifier/simp_rule_set.h
index a372f78dc..0c812d1cf 100644
--- a/src/library/blast/simplifier/simp_rule_set.h
+++ b/src/library/blast/simplifier/simp_rule_set.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "library/tmp_type_context.h"
 #include "library/head_map.h"
 #include "library/io_state_stream.h"
-#include <vector>
 
 #ifndef LEAN_SIMP_DEFAULT_PRIORITY
 #define LEAN_SIMP_DEFAULT_PRIORITY 1000
@@ -146,6 +145,8 @@ bool is_congr_rule(environment const & env, name const & n);
 simp_rule_sets get_simp_rule_sets(environment const & env);
 /** \brief Get simplification rule sets in the given namespace. */
 simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns);
+/** \brief Get simplification rule sets in the given namespaces. */
+simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, std::initializer_list<name> const & nss);
 
 io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s);
 
diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp
index 38517e97f..8fd7b4ecd 100644
--- a/src/library/blast/simplifier/simplifier.cpp
+++ b/src/library/blast/simplifier/simplifier.cpp
@@ -1,7 +1,7 @@
 /*
-  Copyright (c) 2015 Daniel Selsam. All rights reserved.
-  Released under Apache 2.0 license as described in the file LICENSE.
-  Author: Daniel Selsam
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
 */
 #include "kernel/abstract.h"
 #include "kernel/expr_maps.h"
@@ -60,10 +60,11 @@ using simp::result;
 
 /* Names */
 
-static name * g_simplify_empty_namespace     = nullptr;
+static name * g_simplify_prove_namespace     = nullptr;
+static name * g_simplify_neg_namespace       = nullptr;
 static name * g_simplify_unit_namespace      = nullptr;
 static name * g_simplify_ac_namespace        = nullptr;
-static name * g_simplify_som_namespace       = nullptr;
+static name * g_simplify_distrib_namespace   = nullptr;
 static name * g_simplify_numeral_namespace   = nullptr;
 
 /* Options */
@@ -980,7 +981,9 @@ result simplifier::fuse(expr const & e) {
     /* Prove (1) == (3) using simplify with [ac] */
     flet<bool> no_simplify_numerals(m_numerals, false);
     auto pf_1_3 = prove(get_app_builder().mk_eq(e, e_grp),
-                        get_simp_rule_sets(env(), ios(), *g_simplify_ac_namespace));
+                        get_simp_rule_sets(env(), ios(),
+                                           {*g_simplify_prove_namespace, *g_simplify_unit_namespace,
+                                                   *g_simplify_neg_namespace, *g_simplify_ac_namespace}));
     if (!pf_1_3) {
         diagnostic(env(), ios()) << e << "\n\n =?=\n\n" << e_grp << "\n";
         throw blast_exception("Failed to prove (1) == (3) during fusion", e);
@@ -988,7 +991,10 @@ result simplifier::fuse(expr const & e) {
 
     /* Prove (4) == (5) using simplify with [som] */
     auto pf_4_5 = prove(get_app_builder().mk_eq(e_grp_ls, e_fused_ls),
-                        get_simp_rule_sets(env(), ios(), *g_simplify_som_namespace));
+                        get_simp_rule_sets(env(), ios(),
+                                           {*g_simplify_prove_namespace, *g_simplify_unit_namespace,
+                                                   *g_simplify_neg_namespace, *g_simplify_ac_namespace,
+                                                   *g_simplify_distrib_namespace}));
     if (!pf_4_5) {
         diagnostic(env(), ios()) << e_grp_ls << "\n\n =?=\n\n" << e_fused_ls << "\n";
         throw blast_exception("Failed to prove (4) == (5) during fusion", e);
@@ -996,7 +1002,9 @@ result simplifier::fuse(expr const & e) {
 
     /* Prove (5) == (6) using simplify with [numeral] */
     flet<bool> simplify_numerals(m_numerals, true);
-    result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(), *g_simplify_ac_namespace));
+    result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(),
+                                                               {*g_simplify_unit_namespace, *g_simplify_neg_namespace,
+                                                                       *g_simplify_ac_namespace}));
 
     /* Prove (4) == (6) by transitivity of proofs (2) and (3) */
     expr pf_4_6;
@@ -1049,10 +1057,11 @@ expr_pair simplifier::split_summand(expr const & e, expr const & f_mul, expr con
 /* Setup and teardown */
 
 void initialize_simplifier() {
-    g_simplify_empty_namespace     = new name{"simplifier", "empty"};
+    g_simplify_prove_namespace     = new name{"simplifier", "prove"};
+    g_simplify_neg_namespace       = new name{"simplifier", "neg"};
     g_simplify_unit_namespace      = new name{"simplifier", "unit"};
     g_simplify_ac_namespace        = new name{"simplifier", "ac"};
-    g_simplify_som_namespace       = new name{"simplifier", "som"};
+    g_simplify_distrib_namespace   = new name{"simplifier", "distrib"};
     g_simplify_numeral_namespace   = new name{"simplifier", "numeral"};
 
     g_simplify_max_steps     = new name{"simplify", "max_steps"};
@@ -1097,10 +1106,11 @@ void finalize_simplifier() {
     delete g_simplify_max_steps;
 
     delete g_simplify_numeral_namespace;
-    delete g_simplify_som_namespace;
+    delete g_simplify_distrib_namespace;
     delete g_simplify_ac_namespace;
     delete g_simplify_unit_namespace;
-    delete g_simplify_empty_namespace;
+    delete g_simplify_neg_namespace;
+    delete g_simplify_prove_namespace;
 }
 
 /* Entry points */
diff --git a/tests/lean/simplifier12.lean b/tests/lean/simplifier12.lean
index b2ccd19e0..d402c6bcc 100644
--- a/tests/lean/simplifier12.lean
+++ b/tests/lean/simplifier12.lean
@@ -1,5 +1,5 @@
-import algebra.simplifier
-open algebra simplifier.som
+import algebra.ring
+open algebra
 
 set_option simplify.max_steps 1000
 universe l
@@ -7,4 +7,6 @@ constants (T : Type.{l}) (s : algebra.comm_ring T)
 constants (x1 x2 x3 x4 : T) (f g : T → T)
 attribute s [instance]
 
-#simplify eq simplifier.som 0 x2 + (1 * g x1 + 0 + (f x3 * 3 * 1 * (x2 + 0 + g x1 * 7) * x2 * 1)) + 5 * (x4 + f x1)
+open simplifier.unit simplifier.ac simplifier.neg simplifier.distrib
+
+#simplify eq env 0 x2 + (1 * g x1 + 0 + (f x3 * 3 * 1 * (x2 + 0 + g x1 * 7) * x2 * 1)) + 5 * (x4 + f x1)
diff --git a/tests/lean/simplifier14.lean b/tests/lean/simplifier14.lean
index 0841c666a..06488b661 100644
--- a/tests/lean/simplifier14.lean
+++ b/tests/lean/simplifier14.lean
@@ -1,5 +1,5 @@
 -- Basic fusion
-import algebra.simplifier
+import algebra.ring algebra.numeral
 open algebra
 
 universe l
@@ -9,19 +9,21 @@ attribute s [instance]
 set_option simplify.max_steps 50000
 set_option simplify.fuse true
 
-#simplify eq simplifier.som 0 x1
-#simplify eq simplifier.som 0 x1 + x1
-#simplify eq simplifier.som 0 (x1 + x1) + x1
-#simplify eq simplifier.som 0 (x1 + x1) + (x1 + x1)
-#simplify eq simplifier.som 0 x1 + x1 + x1 + x1
-#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1
-#simplify eq simplifier.som 0 x1 - x1
-#simplify eq simplifier.som 0 (x1 - x1) + x1
-#simplify eq simplifier.som 0 (x1 + x1) - (x1 + x1)
-#simplify eq simplifier.som 0 x1 + x1 - x1 - x1
-#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1
-#simplify eq simplifier.som 0 (x1 - x2) + x2 - x1
-#simplify eq simplifier.som 0 (x1 + x1 + x2 + x1) - 2* x2 + 1 * x2 - 3 * x1
-#simplify eq simplifier.som 0 x2 + x1 - x2 - - x1
-#simplify eq simplifier.som 0 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2
-#simplify eq simplifier.som 0 x2 + x1 - x2 - (- x1)
+open simplifier.unit simplifier.ac simplifier.neg
+
+#simplify eq env 0 x1
+#simplify eq env 0 x1 + x1
+#simplify eq env 0 (x1 + x1) + x1
+#simplify eq env 0 (x1 + x1) + (x1 + x1)
+#simplify eq env 0 x1 + x1 + x1 + x1
+#simplify eq env 0 x1 + x1 + (x1 + x1) + x1
+#simplify eq env 0 x1 - x1
+#simplify eq env 0 (x1 - x1) + x1
+#simplify eq env 0 (x1 + x1) - (x1 + x1)
+#simplify eq env 0 x1 + x1 - x1 - x1
+#simplify eq env 0 x1 + x1 + (x1 + x1) + x1
+#simplify eq env 0 (x1 - x2) + x2 - x1
+#simplify eq env 0 (x1 + x1 + x2 + x1) - 2* x2 + 1 * x2 - 3 * x1
+#simplify eq env 0 x2 + x1 - x2 - - x1
+#simplify eq env 0 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2
+#simplify eq env 0 x2 + x1 - x2 - (- x1)
diff --git a/tests/lean/simplifier15.lean b/tests/lean/simplifier15.lean
index 6f619b176..5f6442cc0 100644
--- a/tests/lean/simplifier15.lean
+++ b/tests/lean/simplifier15.lean
@@ -1,5 +1,5 @@
 -- normalizing reducible non-subsingleton instances
-import algebra.simplifier
+import algebra.ring
 open algebra
 
 universe l
diff --git a/tests/lean/simplifier18.lean b/tests/lean/simplifier18.lean
index 41ba4bc21..d5a9ef3ee 100644
--- a/tests/lean/simplifier18.lean
+++ b/tests/lean/simplifier18.lean
@@ -1,5 +1,5 @@
 -- Basic fusion
-import algebra.simplifier
+import algebra.ring algebra.numeral
 open algebra
 
 universe l
@@ -9,19 +9,21 @@ attribute s [instance]
 set_option simplify.max_steps 50000
 set_option simplify.fuse true
 
-#simplify eq simplifier.som 0 x1 * x2
-#simplify eq simplifier.som 0 x1 * 2 * x2
-#simplify eq simplifier.som 0 x1 * 2 * x2 * 3
-#simplify eq simplifier.som 0 2 * x2 + x1 * 8 * x2 * 4
-#simplify eq simplifier.som 0 2 * x2 - x1 * 8 * x2 * 4
-#simplify eq simplifier.som 0 2 * x2 - 8 * x2 * 4 * x1
-#simplify eq simplifier.som 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2
-#simplify eq simplifier.som 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3
-#simplify eq simplifier.som 0 2 * 2 + x1
-#simplify eq simplifier.som 0 x2 * (2 * 2) + x1
-#simplify eq simplifier.som 0 2 * 2 * x2 + x1
-#simplify eq simplifier.som 0 2 * x2 * 2 + x1
-#simplify eq simplifier.som 0 200 * x2 * 200 + x1
-#simplify eq simplifier.som 0 x1 * 200 * x2 * 200 + x1
-#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * 200 + x1
-#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * x4 * 200 + x1
+open simplifier.unit simplifier.ac simplifier.neg
+
+#simplify eq env 0 x1 * x2
+#simplify eq env 0 x1 * 2 * x2
+#simplify eq env 0 x1 * 2 * x2 * 3
+#simplify eq env 0 2 * x2 + x1 * 8 * x2 * 4
+#simplify eq env 0 2 * x2 - x1 * 8 * x2 * 4
+#simplify eq env 0 2 * x2 - 8 * x2 * 4 * x1
+#simplify eq env 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2
+#simplify eq env 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3
+#simplify eq env 0 2 * 2 + x1
+#simplify eq env 0 x2 * (2 * 2) + x1
+#simplify eq env 0 2 * 2 * x2 + x1
+#simplify eq env 0 2 * x2 * 2 + x1
+#simplify eq env 0 200 * x2 * 200 + x1
+#simplify eq env 0 x1 * 200 * x2 * 200 + x1
+#simplify eq env 0 x1 * 200 * x2 * x3 * 200 + x1
+#simplify eq env 0 x1 * 200 * x2 * x3 * x4 * 200 + x1
diff --git a/tests/lean/simplifier19.lean b/tests/lean/simplifier19.lean
index ced40ce92..0b6190023 100644
--- a/tests/lean/simplifier19.lean
+++ b/tests/lean/simplifier19.lean
@@ -1,5 +1,5 @@
 -- Nested fusion
-import algebra.simplifier
+import algebra.ring algebra.numeral
 open algebra
 
 universe l
@@ -9,4 +9,6 @@ attribute s [instance]
 set_option simplify.max_steps 50000
 set_option simplify.fuse true
 
-#simplify eq simplifier.som 0 f (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) + g (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2)
+open simplifier.unit simplifier.ac simplifier.neg
+
+#simplify eq env 0 f (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) + g (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2)
diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean
index 2c178da39..3227ea847 100644
--- a/tests/lean/simplifier_light.lean
+++ b/tests/lean/simplifier_light.lean
@@ -1,8 +1,8 @@
 -- Test [light] annotation
 -- Remark: it will take some additional work to get ⁻¹ to rewrite well
 -- when there is a proof obligation.
-import algebra.simplifier algebra.field data.set data.finset
-open algebra simplifier.ac
+import algebra.ring algebra.field data.set data.finset
+open algebra
 attribute neg [light 2]
 attribute inv [light 2]
 
@@ -12,6 +12,8 @@ attribute add_neg_cancel_left [simp]
 attribute mul.right_inv [simp]
 attribute mul_inv_cancel_left [simp]
 
+open simplifier.unit simplifier.ac
+
 namespace ag
 universe l
 constants (A : Type.{l}) (s1 : add_comm_group A) (s2 : has_one A)
diff --git a/tests/lean/simplifier_norm_num.lean b/tests/lean/simplifier_norm_num.lean
index 2d3eb385f..d72d93370 100644
--- a/tests/lean/simplifier_norm_num.lean
+++ b/tests/lean/simplifier_norm_num.lean
@@ -1,9 +1,10 @@
-import algebra.simplifier
+import algebra.ring algebra.numeral
 open algebra
 
-open simplifier.numeral
-
 set_option simplify.max_steps 5000000
+-- TODO(dhs): we need to create the simplifier.numeral namespace incrementally.
+-- Once it exists, we can uncomment the following line to use it simplify.
+set_option simplify.numerals true
 universe l
 constants (A : Type.{l}) (A_comm_ring : comm_ring A)
 attribute A_comm_ring [instance]
@@ -54,5 +55,4 @@ attribute A_comm_ring [instance]
 
 #simplify eq env 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733)
 
--- The following test is too slow
--- #simplify eq 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536
+#simplify eq env 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536
diff --git a/tests/lean/simplifier_norm_num.lean.expected.out b/tests/lean/simplifier_norm_num.lean.expected.out
index 3b82bbf47..d66457d0b 100644
--- a/tests/lean/simplifier_norm_num.lean.expected.out
+++ b/tests/lean/simplifier_norm_num.lean.expected.out
@@ -40,3 +40,4 @@
 90
 15241383936
 130049014430002489296
+6599110652246543565516387775250463433475607911914556819497064648