diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp
index 8f12c511c1..0797b75976 100644
--- a/src/library/norm_num.cpp
+++ b/src/library/norm_num.cpp
@@ -7,43 +7,42 @@ Author: Robert Y. Lewis
 #include "library/norm_num.h"
 #include "library/constants.h"
 namespace lean {
-  static name * g_add           = nullptr,
-              * g_add1          = nullptr,
-              * g_mul           = nullptr,
-              * g_sub           = nullptr,
-              * g_bit0_add_bit0 = nullptr,
-              * g_bit1_add_bit0 = nullptr,
-              * g_bit0_add_bit1 = nullptr,
-              * g_bit1_add_bit1 = nullptr,
-              * g_bin_add_0     = nullptr,
-              * g_bin_0_add     = nullptr,
-              * g_bin_add_1     = nullptr,
-              * g_1_add_bit0    = nullptr,
-              * g_bit0_add_1    = nullptr,
-              * g_bit1_add_1    = nullptr,
-              * g_1_add_bit1    = nullptr,
-              * g_one_add_one   = nullptr,
-              * g_add1_bit0     = nullptr,
-              * g_add1_bit1     = nullptr,
-              * g_add1_zero     = nullptr,
-              * g_add1_one      = nullptr,
-              * g_subst_sum     = nullptr,
-              * g_subst_prod    = nullptr,
-              * g_mk_cong       = nullptr,
-              * g_mk_eq         = nullptr,
-              * g_mul_zero      = nullptr,
-              * g_zero_mul      = nullptr,
-              * g_mul_one       = nullptr,
-              * g_mul_bit0      = nullptr,
-              * g_mul_bit1      = nullptr,
-              * g_has_mul       = nullptr,
-              * g_add_monoid    = nullptr,
-              * g_monoid        = nullptr,
-              * g_add_comm      = nullptr,
-              * g_mul_zero_class= nullptr,
-              * g_distrib       = nullptr,
-              * g_semiring      = nullptr;
-
+static name * g_add           = nullptr,
+    * g_add1          = nullptr,
+    * g_mul           = nullptr,
+    * g_sub           = nullptr,
+    * g_bit0_add_bit0 = nullptr,
+    * g_bit1_add_bit0 = nullptr,
+    * g_bit0_add_bit1 = nullptr,
+    * g_bit1_add_bit1 = nullptr,
+    * g_bin_add_0     = nullptr,
+    * g_bin_0_add     = nullptr,
+    * g_bin_add_1     = nullptr,
+    * g_1_add_bit0    = nullptr,
+    * g_bit0_add_1    = nullptr,
+    * g_bit1_add_1    = nullptr,
+    * g_1_add_bit1    = nullptr,
+    * g_one_add_one   = nullptr,
+    * g_add1_bit0     = nullptr,
+    * g_add1_bit1     = nullptr,
+    * g_add1_zero     = nullptr,
+    * g_add1_one      = nullptr,
+    * g_subst_sum     = nullptr,
+    * g_subst_prod    = nullptr,
+    * g_mk_cong       = nullptr,
+    * g_mk_eq         = nullptr,
+    * g_mul_zero      = nullptr,
+    * g_zero_mul      = nullptr,
+    * g_mul_one       = nullptr,
+    * g_mul_bit0      = nullptr,
+    * g_mul_bit1      = nullptr,
+    * g_has_mul       = nullptr,
+    * g_add_monoid    = nullptr,
+    * g_monoid        = nullptr,
+    * g_add_comm      = nullptr,
+    * g_mul_zero_class = nullptr,
+    * g_distrib       = nullptr,
+    * g_semiring      = nullptr;
 
 static bool is_numeral_aux(expr const & e, bool is_first) {
     buffer<expr> args;
@@ -280,8 +279,7 @@ pair<expr, expr> norm_num_context::mk_norm_add(expr const & lhs, expr const & rh
     } else if (is_zero(rhs)) {
         rv = lhs;
         prf = mk_app({mk_const(*g_bin_add_0), type, mk_add_monoid(typec), lhs});
-    }
-    else {
+    } else {
       std::cout << "\n\n bad args: " << lhs_head << ", " << rhs_head << "\n";
       throw exception("mk_norm_add got malformed args");
     }
@@ -367,80 +365,80 @@ pair<expr, expr> norm_num_context::mk_norm_sub(expr const &, expr const &) {
 }
 
 void initialize_norm_num() {
-  g_add     = new name("add");
-  g_add1    = new name("add1");
-  g_mul     = new name("mul");
-  g_sub     = new name("sub");
-  g_bit0_add_bit0 = new name("bit0_add_bit0_helper");
-  g_bit1_add_bit0 = new name("bit1_add_bit0_helper");
-  g_bit0_add_bit1 = new name("bit0_add_bit1_helper");
-  g_bit1_add_bit1 = new name("bit1_add_bit1_helper");
-  g_bin_add_0     = new name("bin_add_zero");
-  g_bin_0_add     = new name("bin_zero_add");
-  g_bin_add_1     = new name("bin_add_one");
-  g_1_add_bit0    = new name("one_add_bit0");
-  g_bit0_add_1    = new name("bit0_add_one");
-  g_bit1_add_1    = new name("bit1_add_one_helper");
-  g_1_add_bit1    = new name("one_add_bit1_helper");
-  g_one_add_one   = new name("one_add_one");
-  g_add1_bit0     = new name("add1_bit0");
-  g_add1_bit1     = new name("add1_bit1_helper");
-  g_add1_zero     = new name("add1_zero");
-  g_add1_one      = new name("add1_one");
-  g_subst_sum     = new name("subst_into_sum");
-  g_subst_prod    = new name("subst_into_prod");
-  g_mk_cong       = new name("mk_cong");
-  g_mk_eq         = new name("mk_eq");
-  g_zero_mul      = new name("zero_mul");
-  g_mul_zero      = new name("mul_zero");
-  g_mul_one       = new name("mul_one");
-  g_mul_bit0      = new name("mul_bit0_helper");
-  g_mul_bit1      = new name("mul_bit1_helper");
-  g_has_mul       = new name("has_mul");
-  g_add_monoid        = new name("algebra", "add_monoid");
-  g_monoid        = new name("algebra", "monoid");
-  g_add_comm      = new name("algebra", "add_comm_semigroup");
-  g_mul_zero_class      = new name("algebra", "mul_zero_class");
-  g_distrib       = new name("algebra", "distrib");
-  g_semiring      = new name("algebra", "semiring");
+    g_add     = new name("add");
+    g_add1    = new name("add1");
+    g_mul     = new name("mul");
+    g_sub     = new name("sub");
+    g_bit0_add_bit0 = new name("bit0_add_bit0_helper");
+    g_bit1_add_bit0 = new name("bit1_add_bit0_helper");
+    g_bit0_add_bit1 = new name("bit0_add_bit1_helper");
+    g_bit1_add_bit1 = new name("bit1_add_bit1_helper");
+    g_bin_add_0     = new name("bin_add_zero");
+    g_bin_0_add     = new name("bin_zero_add");
+    g_bin_add_1     = new name("bin_add_one");
+    g_1_add_bit0    = new name("one_add_bit0");
+    g_bit0_add_1    = new name("bit0_add_one");
+    g_bit1_add_1    = new name("bit1_add_one_helper");
+    g_1_add_bit1    = new name("one_add_bit1_helper");
+    g_one_add_one   = new name("one_add_one");
+    g_add1_bit0     = new name("add1_bit0");
+    g_add1_bit1     = new name("add1_bit1_helper");
+    g_add1_zero     = new name("add1_zero");
+    g_add1_one      = new name("add1_one");
+    g_subst_sum     = new name("subst_into_sum");
+    g_subst_prod    = new name("subst_into_prod");
+    g_mk_cong       = new name("mk_cong");
+    g_mk_eq         = new name("mk_eq");
+    g_zero_mul      = new name("zero_mul");
+    g_mul_zero      = new name("mul_zero");
+    g_mul_one       = new name("mul_one");
+    g_mul_bit0      = new name("mul_bit0_helper");
+    g_mul_bit1      = new name("mul_bit1_helper");
+    g_has_mul       = new name("has_mul");
+    g_add_monoid        = new name("algebra", "add_monoid");
+    g_monoid        = new name("algebra", "monoid");
+    g_add_comm      = new name("algebra", "add_comm_semigroup");
+    g_mul_zero_class      = new name("algebra", "mul_zero_class");
+    g_distrib       = new name("algebra", "distrib");
+    g_semiring      = new name("algebra", "semiring");
 }
 
 void finalize_norm_num() {
-  delete g_add;
-  delete g_add1;
-  delete g_mul;
-  delete g_sub;
-  delete g_bit0_add_bit0;
-  delete g_bit1_add_bit0;
-  delete g_bit0_add_bit1;
-  delete g_bit1_add_bit1;
-  delete g_bin_add_0;
-  delete g_bin_0_add;
-  delete g_bin_add_1;
-  delete g_1_add_bit0;
-  delete g_bit0_add_1;
-  delete g_bit1_add_1;
-  delete g_1_add_bit1;
-  delete g_one_add_one;
-  delete g_add1_bit0;
-  delete g_add1_bit1;
-  delete g_add1_zero;
-  delete g_add1_one;
-  delete g_subst_sum;
-  delete g_subst_prod;
-  delete g_mk_cong;
-  delete g_mk_eq;
-  delete g_mul_zero;
-  delete g_zero_mul;
-  delete g_mul_one;
-  delete g_mul_bit0;
-  delete g_mul_bit1;
-  delete g_has_mul;
-  delete g_add_monoid;
-  delete g_monoid;
-  delete g_add_comm;
-  delete g_mul_zero_class;
-  delete g_distrib;
-  delete g_semiring;
+    delete g_add;
+    delete g_add1;
+    delete g_mul;
+    delete g_sub;
+    delete g_bit0_add_bit0;
+    delete g_bit1_add_bit0;
+    delete g_bit0_add_bit1;
+    delete g_bit1_add_bit1;
+    delete g_bin_add_0;
+    delete g_bin_0_add;
+    delete g_bin_add_1;
+    delete g_1_add_bit0;
+    delete g_bit0_add_1;
+    delete g_bit1_add_1;
+    delete g_1_add_bit1;
+    delete g_one_add_one;
+    delete g_add1_bit0;
+    delete g_add1_bit1;
+    delete g_add1_zero;
+    delete g_add1_one;
+    delete g_subst_sum;
+    delete g_subst_prod;
+    delete g_mk_cong;
+    delete g_mk_eq;
+    delete g_mul_zero;
+    delete g_zero_mul;
+    delete g_mul_one;
+    delete g_mul_bit0;
+    delete g_mul_bit1;
+    delete g_has_mul;
+    delete g_add_monoid;
+    delete g_monoid;
+    delete g_add_comm;
+    delete g_mul_zero_class;
+    delete g_distrib;
+    delete g_semiring;
 }
 }
diff --git a/src/library/norm_num.h b/src/library/norm_num.h
index 491abc80a6..68fd66cd8d 100644
--- a/src/library/norm_num.h
+++ b/src/library/norm_num.h
@@ -17,8 +17,8 @@ class norm_num_context {
     pair<expr, expr> mk_norm_add(expr const &, expr const &);
     pair<expr, expr> mk_norm_add1(expr const &);
     pair<expr, expr> mk_norm_mul(expr const &, expr const &);
-    pair<expr, expr> mk_norm_div(expr const &, expr const &);    
-    pair<expr, expr> mk_norm_sub(expr const &, expr const &);  
+    pair<expr, expr> mk_norm_div(expr const &, expr const &);
+    pair<expr, expr> mk_norm_sub(expr const &, expr const &);
     expr mk_const(name const & n);
     expr mk_cong(expr const &, expr const &, expr const &, expr const &, expr const &);
     expr mk_has_add(expr const &);
diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp
index 01a18d476a..7a1d843760 100644
--- a/src/library/tactic/norm_num_tactic.cpp
+++ b/src/library/tactic/norm_num_tactic.cpp
@@ -25,9 +25,9 @@ tactic norm_num_tactic() {
                 throw_tactic_exception_if_enabled(s, "norm_num tactic failed, conclusion is not an equality");
                 return none_proof_state();
             }
-	    type_checker_ptr rtc = mk_type_checker(env, UnfoldReducible);
-	    lhs = normalize(*rtc, lhs);
-	    rhs = normalize(*rtc, rhs);
+            type_checker_ptr rtc = mk_type_checker(env, UnfoldReducible);
+            lhs = normalize(*rtc, lhs);
+            rhs = normalize(*rtc, rhs);
 
             buffer<expr> hyps;
             g.get_hyps(hyps);
@@ -36,26 +36,26 @@ tactic norm_num_tactic() {
                 pair<expr, expr> p = mk_norm_num(env, ctx, lhs);
                 expr new_lhs = p.first;
                 expr new_lhs_pr  = p.second;
-		pair<expr, expr> p2 = mk_norm_num(env, ctx, rhs);
-		expr new_rhs = p2.first;
-		expr new_rhs_pr = p2.second;
-		auto v_lhs = to_num(new_lhs), v_rhs = to_num(new_rhs);
-		if (v_lhs && v_rhs) {
-		  if ( *v_lhs == *v_rhs) {
-		    type_checker tc(env);
-		    expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
-		    substitution new_subst = s.get_subst();
-		    assign(new_subst, g, g_prf);
-		    return some_proof_state(proof_state(s, tail(gs), new_subst));
-		  } else {
-		    std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n";
-		    throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs doesn't match rhs");
-		    return none_proof_state();
-		  }
-		} else {
-		  throw_tactic_exception_if_enabled(s, "norm_num tactic failed, one side is not a numeral");
-		  return none_proof_state();
-		}
+                pair<expr, expr> p2 = mk_norm_num(env, ctx, rhs);
+                expr new_rhs = p2.first;
+                expr new_rhs_pr = p2.second;
+                auto v_lhs = to_num(new_lhs), v_rhs = to_num(new_rhs);
+                if (v_lhs && v_rhs) {
+                    if (*v_lhs == *v_rhs) {
+                        type_checker tc(env);
+                        expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
+                        substitution new_subst = s.get_subst();
+                        assign(new_subst, g, g_prf);
+                        return some_proof_state(proof_state(s, tail(gs), new_subst));
+                    } else {
+                        std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n";
+                        throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs doesn't match rhs");
+                        return none_proof_state();
+                    }
+                } else {
+                    throw_tactic_exception_if_enabled(s, "norm_num tactic failed, one side is not a numeral");
+                    return none_proof_state();
+                }
             } catch (exception & ex) {
                 throw_tactic_exception_if_enabled(s, ex.what());
                 return none_proof_state();