diff --git a/library/algebra/simplifier.lean b/library/algebra/simplifier.lean
index a58630ad7..8f7d4d6c6 100644
--- a/library/algebra/simplifier.lean
+++ b/library/algebra/simplifier.lean
@@ -37,45 +37,63 @@ end units
 
 -- TODO(dhs): remove `add1` from the original lemmas and delete this
 namespace numeral_helper
-open algebra norm_num
+open algebra
 
-theorem bit1_add_bit1 {A : Type} [s : algebra.add_comm_semigroup A]
+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)
-  := bit1_add_bit1 a b
-
-theorem one_add_bit1 {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A)
-  : one + bit1 a = (bit1 a) + 1 := !add.comm
+  := 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) := add1_bit1 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
 
 namespace numeral
 
-attribute norm_num.one_add_bit0 [simp]
-attribute norm_num.bit0_add_one [simp]
-attribute numeral_helper.one_add_bit1 [simp]
-attribute numeral_helper.bit1_add_one [simp]
-attribute norm_num.one_add_one [simp]
-
 attribute norm_num.bit0_add_bit0 [simp]
-attribute norm_num.bit0_add_bit1 [simp]
+attribute numeral_helper.bit1_add_one [simp]
 attribute norm_num.bit1_add_bit0 [simp]
-
 attribute numeral_helper.bit1_add_bit1 [simp]
-
-attribute algebra.one_mul [simp]
-attribute algebra.mul_one [simp]
-
-attribute norm_num.mul_bit0 [simp]
-attribute norm_num.mul_bit1 [simp]
+attribute norm_num.bit0_add_bit1 [simp]
+attribute numeral_helper.one_add_bit1 [simp]
 
 attribute algebra.zero_add [simp]
 attribute algebra.add_zero [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]
+
 attribute algebra.zero_mul [simp]
 attribute algebra.mul_zero [simp]
+attribute algebra.one_mul [simp]
+attribute algebra.mul_one [simp]
 
 end numeral
 
diff --git a/tests/lean/simplifier_norm_num.lean b/tests/lean/simplifier_norm_num.lean
index 1e6ee0a1c..027608b6a 100644
--- a/tests/lean/simplifier_norm_num.lean
+++ b/tests/lean/simplifier_norm_num.lean
@@ -1,9 +1,11 @@
 import algebra.simplifier
-open simplifier.numeral
 open algebra
 
-set_option simplify.max_steps 500000
-constants (A : Type.{1}) (A_comm_ring : algebra.comm_ring A)
+open simplifier.numeral
+
+set_option simplify.max_steps 5000000
+universe l
+constants (A : Type.{l}) (A_comm_ring : comm_ring A)
 attribute A_comm_ring [instance]
 
 #simplify eq 0 (0:A) + 1
@@ -27,6 +29,7 @@ attribute A_comm_ring [instance]
 #simplify eq 0 (5:A) + 28
 #simplify eq 0 (0 : A) + (2 + 3) + 7
 #simplify eq 0 (70 : A) + (33 + 2)
+
 #simplify eq 0 (23000000000 : A) + 22000000000
 
 #simplify eq 0 (0 : A) * 0