diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 64005d306c..7ca817e79d 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -1316,13 +1316,13 @@ static environment congr_lemma_cmd(parser & p) {
 static environment simplify_cmd(parser & p) {
     name rel = p.check_constant_next("invalid #simplify command, constant expected");
     unsigned o = p.parse_small_nat();
-    
+
     expr e; level_param_names ls;
     std::tie(e, ls) = parse_local_expr(p);
 
-    blast::scope_debug scope(p.env(),p.ios());
+    blast::scope_debug scope(p.env(), p.ios());
     blast::branch b;
-    blast::simp::result r = blast::simplify(b,rel,e);
+    blast::simp::result r = blast::simplify(b, rel, e);
 
     flycheck_information info(p.regular_stream());
     if (info.enabled()) {
@@ -1332,10 +1332,9 @@ static environment simplify_cmd(parser & p) {
 
     if (r.is_none()) {
         p.regular_stream() << "<refl>" << endl;
-    }
-    else {
+    } else {
         auto tc = mk_type_checker(p.env(), p.mk_ngen());
-        
+
         expr pf_type = tc->check(r.get_proof(), ls).first;
 
         if (o == 0) p.regular_stream() << r.get_new() << endl;
@@ -1379,7 +1378,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("#accessible",       "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
     add_cmd(r, cmd_info("#decl_stats",       "(for debugging purposes) display declaration statistics", decl_stats_cmd));
     add_cmd(r, cmd_info("#relevant_thms",    "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));
-    add_cmd(r, cmd_info("#simplify",         "(for debugging purposes) simplify given expression", simplify_cmd));    
+    add_cmd(r, cmd_info("#simplify",         "(for debugging purposes) simplify given expression", simplify_cmd));
 
     register_decl_cmds(r);
     register_inductive_cmd(r);
diff --git a/src/library/blast/init_module.cpp b/src/library/blast/init_module.cpp
index 3beb0449c2..406d03132c 100644
--- a/src/library/blast/init_module.cpp
+++ b/src/library/blast/init_module.cpp
@@ -20,7 +20,7 @@ void initialize_blast_module() {
 }
 void finalize_blast_module() {
     finalize_blast_tactic();
-    blast::finalize_simplifier();    
+    blast::finalize_simplifier();
     finalize_blast();
     blast::finalize_branch();
     blast::finalize_expr();
diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index 88af4c01d2..f0df422cf2 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -22,7 +22,6 @@ Author: Daniel Selsam
 #include "util/sexpr/option_declarations.h"
 #include <array>
 #include <map>
-#include <iostream> // TODO just for occasional debugging
 
 #ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
 #define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 100
@@ -111,11 +110,11 @@ class simplifier {
     bool                                         m_contextual{get_simplify_contextual()};
     bool                                         m_expand_macros{get_simplify_expand_macros()};
     bool                                         m_trace{get_simplify_trace()};
-    
+
     /* Cache */
-    typedef expr_bi_struct_map<result>                   simplify_cache;
-    typedef std::map<name,simplify_cache,name_quick_cmp> simplify_caches;
-    simplify_caches                                      m_simplify_caches;
+    typedef expr_bi_struct_map<result>                     simplify_cache;
+    typedef std::map<name, simplify_cache, name_quick_cmp> simplify_caches;
+    simplify_caches                                        m_simplify_caches;
 
     optional<result> cache_lookup(expr const & e);
     void cache_save(expr const & e, result const & r);
@@ -132,45 +131,44 @@ class simplifier {
     simp_rule_sets add_to_srss(simp_rule_sets const & _srss, buffer<expr> & ls) {
         simp_rule_sets srss = _srss;
         for (unsigned i = 0; i < ls.size(); i++) {
-            // TODO assert no metas?
+            // TODO(dhs): assert no metas
             expr & l = ls[i];
-            tmp_type_context tctx(env(),ios());
-            srss = add(tctx,srss,mlocal_name(l),tctx.infer(l),l);
+            tmp_type_context tctx(env(), ios());
+            srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
         }
         return srss;
     }
 
     /* Results */
     result lift_from_eq(expr const & x, result const & r);
-    result join(result const & r1, result const & r2);        
+    result join(result const & r1, result const & r2);
     result funext(result const & r, expr const & l);
     result finalize(result const & r);
 
     /* Simplification */
-    result simplify(expr const & e);    
+    result simplify(expr const & e);
     result simplify_lambda(expr const & e);
     result simplify_pi(expr const & e);
     result simplify_app(expr const & e);
     result simplify_fun(expr const & e);
-    
+
     /* Rewriting */
     result rewrite(expr const & e);
-    result rewrite(expr const & e, simp_rule_sets const & srss);        
+    result rewrite(expr const & e, simp_rule_sets const & srss);
     result rewrite(expr const & e, simp_rule const & sr);
 
     /* Congruence */
-    result congr(result const & r_f, result const & r_arg);        
+    result congr(result const & r_f, result const & r_arg);
     result congr_fun(result const & r_f, expr const & arg);
     result congr_arg(expr const & f, result const & r_arg);
-    result congr_funs(result const & r_f, buffer<expr> const & args);    
-    
-    result try_congrs(expr const & e);    
+    result congr_funs(result const & r_f, buffer<expr> const & args);
+
+    result try_congrs(expr const & e);
     result try_congr(expr const & e, congr_rule const & cr);
 
 public:
     simplifier(branch const & b, name const & rel);
     result operator()(expr const & e) { return simplify(e); }
-
 };
 
 /* Constructor */
@@ -188,7 +186,7 @@ optional<result> simplifier::cache_lookup(expr const & e) {
 }
 void simplifier::cache_save(expr const & e, result const & r) {
     simplify_cache & cache = m_simplify_caches[m_rel];
-    cache.insert(mk_pair(e,r));
+    cache.insert(mk_pair(e, r));
 }
 
 /* Results */
@@ -197,49 +195,47 @@ result simplifier::lift_from_eq(expr const & x, result const & r) {
     lean_assert(!r.is_none());
 
     expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(x));
-    auto motive_local = m_app_builder.mk_app(m_rel,x,l);
+    auto motive_local = m_app_builder.mk_app(m_rel, x, l);
     lean_assert(motive_local);
 
-    expr motive = Fun(l,*motive_local);
-    
-    auto Rxx = m_app_builder.mk_refl(m_rel,x);
+    expr motive = Fun(l, *motive_local);
+
+    auto Rxx = m_app_builder.mk_refl(m_rel, x);
     lean_assert(Rxx);
 
-    auto pf = m_app_builder.mk_eq_rec(motive,*Rxx,r.get_proof());
-    return result(r.get_new(),pf);
+    auto pf = m_app_builder.mk_eq_rec(motive, *Rxx, r.get_proof());
+    return result(r.get_new(), pf);
 }
 
 result simplifier::join(result const & r1, result const & r2) {
     /* Assumes that both results are with respect to the same relation */
     if (r1.is_none()) {
         return r2;
-    }
-    else if (r2.is_none()) {
+    } else if (r2.is_none()) {
         return r1;
-    }
-    else {
-        auto trans = m_app_builder.mk_trans(m_rel,r1.get_proof(),r2.get_proof());
+    } else {
+        auto trans = m_app_builder.mk_trans(m_rel, r1.get_proof(), r2.get_proof());
         lean_assert(trans);
-        return result(r2.get_new(),*trans);
+        return result(r2.get_new(), *trans);
     }
 }
 
 result simplifier::funext(result const & r, expr const & l) {
     // theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
     lean_assert(!r.is_none());
-    expr e = Fun(l,r.get_new());
-    if (auto pf = m_app_builder.mk_app(get_funext_name(),Fun(l,r.get_proof())))
-        return result(e,*pf);
+    expr e = Fun(l, r.get_new());
+    if (auto pf = m_app_builder.mk_app(get_funext_name(), Fun(l, r.get_proof())))
+        return result(e, *pf);
     else
-        throw blast_exception("failed on [funext] matching",e);
+        throw blast_exception("failed on [funext] matching", e);
 }
 
 result simplifier::finalize(result const & r) {
     if (!r.is_none()) return r;
-    if (auto pf = m_app_builder.mk_refl(m_rel,r.get_new()))
-        return result(r.get_new(),*pf);
+    if (auto pf = m_app_builder.mk_refl(m_rel, r.get_new()))
+        return result(r.get_new(), *pf);
     else
-        throw blast_exception("failed on [refl] matching",r.get_new());
+        throw blast_exception("failed on [refl] matching", r.get_new());
 }
 
 /* Simplification */
@@ -258,7 +254,7 @@ result simplifier::simplify(expr const & e) {
     if (m_memoize) {
         if (auto it = cache_lookup(e)) return *it;
     }
-    
+
     result r(e);
 
     if (m_top_down) r = join(r, rewrite(whnf(r.get_new())));
@@ -276,53 +272,53 @@ result simplifier::simplify(expr const & e) {
         lean_unreachable();
     case expr_kind::Macro:
         if (m_expand_macros) {
-            if (auto m = m_tmp_tctx->expand_macro(e)) r = join(r,simplify(whnf(*m)));
+            if (auto m = m_tmp_tctx->expand_macro(e)) r = join(r, simplify(whnf(*m)));
         }
         break;
     case expr_kind::Lambda:
-        if (using_eq()) r = join(r,simplify_lambda(r.get_new()));
+        if (using_eq()) r = join(r, simplify_lambda(r.get_new()));
         break;
     case expr_kind::Pi:
-        r = join(r,simplify_pi(r.get_new()));
+        r = join(r, simplify_pi(r.get_new()));
         break;
     case expr_kind::App:
-        r = join(r,simplify_app(r.get_new()));
+        r = join(r, simplify_app(r.get_new()));
         break;
     }
 
-    if (!m_top_down) r = join(r,rewrite(whnf(r.get_new())));
+    if (!m_top_down) r = join(r, rewrite(whnf(r.get_new())));
 
     if (r.get_new() == e && !using_eq()) {
         {
             flet<name> use_eq(m_rel, get_eq_name());
             r = simplify(r.get_new());
         }
-        if (!r.is_none()) r = lift_from_eq(e,r);
+        if (!r.is_none()) r = lift_from_eq(e, r);
     }
 
-    if (m_exhaustive && r.get_new() != e) r = join(r,simplify(r.get_new()));
+    if (m_exhaustive && r.get_new() != e) r = join(r, simplify(r.get_new()));
 
-    if (m_memoize) cache_save(e,r);
+    if (m_memoize) cache_save(e, r);
 
     return r;
 }
-    
+
 result simplifier::simplify_lambda(expr const & _e) {
     lean_assert(is_lambda(_e));
     expr e = _e;
-    
+
     buffer<expr> ls;
     while (is_lambda(e)) {
         expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
-        expr l = m_tmp_tctx->mk_tmp_local(d,binding_info(e));
+        expr l = m_tmp_tctx->mk_tmp_local(d, binding_info(e));
         ls.push_back(l);
-        e = instantiate(binding_body(e),l);
+        e = instantiate(binding_body(e), l);
     }
 
     result r = simplify(e);
     if (r.is_none()) { return result(_e); }
 
-    for (int i = ls.size() - 1; i >= 0; --i) r = funext(r,ls[i]);
+    for (int i = ls.size() - 1; i >= 0; --i) r = funext(r, ls[i]);
 
     return r;
 }
@@ -334,17 +330,17 @@ result simplifier::simplify_pi(expr const & e) {
 
 result simplifier::simplify_app(expr const & e) {
     lean_assert(is_app(e));
-    
+
     /* (1) Try user-defined congruences */
     result r = try_congrs(e);
     if (!r.is_none()) {
-        if (using_eq()) return join(r,simplify_fun(r.get_new()));
+        if (using_eq()) return join(r, simplify_fun(r.get_new()));
         else return r;
     }
-    
+
     /* (2) Synthesize congruence lemma */
     if (using_eq()) {
-        // TODO
+        // TODO(dhs): synthesize congruence lemma
     }
 
     /* (3) Fall back on generic binary congruence */
@@ -356,14 +352,13 @@ result simplifier::simplify_app(expr const & e) {
 
         if (is_dependent_fn(f)) {
             if (r_f.is_none()) return e;
-            else return congr_fun(r_f,arg);
-        }
-        else {
+            else return congr_fun(r_f, arg);
+        } else {
             result r_arg = simplify(arg);
             if (r_f.is_none() && r_arg.is_none()) return e;
-            else if (r_f.is_none()) return congr_arg(f,r_arg);
-            else if (r_arg.is_none()) return congr_fun(r_f,arg);            
-            else return congr(r_f,r_arg);
+            else if (r_f.is_none()) return congr_arg(f, r_arg);
+            else if (r_arg.is_none()) return congr_fun(r_f, arg);
+            else return congr(r_f, r_arg);
         }
     }
 
@@ -376,7 +371,7 @@ result simplifier::simplify_fun(expr const & e) {
     expr const & f = get_app_args(e, args);
     result r_f = simplify(f);
     if (r_f.is_none()) return result(e);
-    else return congr_funs(simplify(f),args);
+    else return congr_funs(simplify(f), args);
 }
 
 /* Rewriting */
@@ -384,35 +379,35 @@ result simplifier::simplify_fun(expr const & e) {
 result simplifier::rewrite(expr const & e) {
     result r(e);
     while (true) {
-        result r_ctx = rewrite(r.get_new(),m_ctx_srss);
-        result r_new = rewrite(r_ctx.get_new(),get_simp_rule_sets(env()));
+        result r_ctx = rewrite(r.get_new(), m_ctx_srss);
+        result r_new = rewrite(r_ctx.get_new(), get_simp_rule_sets(env()));
         if (r_ctx.is_none() && r_new.is_none()) break;
-        r = join(join(r,r_ctx),r_new);
+        r = join(join(r, r_ctx), r_new);
     }
     return r;
 }
 
 result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
     result r(e);
-    
+
     simp_rule_set const * sr = srss.find(m_rel);
     if (!sr) return r;
 
     list<simp_rule> const * srs = sr->find_simp(e);
     if (!srs) return r;
 
-    for_each(*srs,[&](simp_rule const & sr) {
-            result r_new = rewrite(r.get_new(),sr);
+    for_each(*srs, [&](simp_rule const & sr) {
+            result r_new = rewrite(r.get_new(), sr);
             if (r_new.is_none()) return;
-            r = join(r,r_new);
+            r = join(r, r_new);
         });
     return r;
 }
 
 result simplifier::rewrite(expr const & e, simp_rule const & sr) {
-    blast_tmp_type_context tmp_tctx(sr.get_num_umeta(),sr.get_num_emeta());
+    blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta());
 
-    if (!tmp_tctx->is_def_eq(e,sr.get_lhs())) return result(e);
+    if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e);
 
     if (m_trace) {
         expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
@@ -448,12 +443,12 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
 
         expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
         if (tmp_tctx->is_prop(m_type)) {
-            flet<name> set_name(m_rel,get_iff_name());
+            flet<name> set_name(m_rel, get_iff_name());
             result r_cond = simplify(m_type);
             if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) {
-                auto pf = m_app_builder.mk_app(name("iff","elim_right"),finalize(r_cond).get_proof(),mk_constant(get_true_intro_name()));
+                auto pf = m_app_builder.mk_app(name("iff", "elim_right"), finalize(r_cond).get_proof(), mk_constant(get_true_intro_name()));
                 lean_assert(pf);
-                bool success = tmp_tctx->is_def_eq(m,*pf);
+                bool success = tmp_tctx->is_def_eq(m, *pf);
                 lean_assert(success);
                 continue;
             }
@@ -475,12 +470,12 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
     expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
 
     if (sr.is_perm()) {
-        if (!is_lt(new_rhs,new_lhs,false))
+        if (!is_lt(new_rhs, new_lhs, false))
             return result(e);
     }
 
     expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof());
-    return result(result(new_rhs,pf));
+    return result(result(new_rhs, pf));
 }
 
 
@@ -490,31 +485,31 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
 result simplifier::congr(result const & r_f, result const & r_arg) {
     lean_assert(!r_f.is_none() && !r_arg.is_none());
     // theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
-    expr e = mk_app(r_f.get_new(),r_arg.get_new());
-    if (auto pf = m_app_builder.mk_app(get_congr_name(),r_f.get_proof(),r_arg.get_proof()))
-        return result(e,*pf);
+    expr e = mk_app(r_f.get_new(), r_arg.get_new());
+    if (auto pf = m_app_builder.mk_app(get_congr_name(), r_f.get_proof(), r_arg.get_proof()))
+        return result(e, *pf);
     else
-        throw blast_exception("failed on [congr] matching",e);
+        throw blast_exception("failed on [congr] matching", e);
 }
 
 result simplifier::congr_fun(result const & r_f, expr const & arg) {
     lean_assert(!r_f.is_none());
     // theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
-    expr e = mk_app(r_f.get_new(),arg);
-    if (auto pf = m_app_builder.mk_app(get_congr_fun_name(),r_f.get_proof(),arg))
-        return result(e,*pf);
+    expr e = mk_app(r_f.get_new(), arg);
+    if (auto pf = m_app_builder.mk_app(get_congr_fun_name(), r_f.get_proof(), arg))
+        return result(e, *pf);
     else
-        throw blast_exception("failed on [congr_fun] matching",e);        
+        throw blast_exception("failed on [congr_fun] matching", e);
 }
 
 result simplifier::congr_arg(expr const & f, result const & r_arg) {
     lean_assert(!r_arg.is_none());
     // theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
-    expr e = mk_app(f,r_arg.get_new());
-    if (auto pf = m_app_builder.mk_app(get_congr_arg_name(),f,r_arg.get_proof()))
-        return result(e,*pf);
+    expr e = mk_app(f, r_arg.get_new());
+    if (auto pf = m_app_builder.mk_app(get_congr_arg_name(), f, r_arg.get_proof()))
+        return result(e, *pf);
     else
-        throw blast_exception("failed on [congr_arg] matching",e);                
+        throw blast_exception("failed on [congr_arg] matching", e);
 }
 
 result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
@@ -523,12 +518,12 @@ result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
     expr e = r_f.get_new();
     expr pf = r_f.get_proof();
     for (unsigned i = 0; i < args.size(); ++i) {
-        e = mk_app(e,args[i]);
-        auto p = m_app_builder.mk_app(get_congr_fun_name(),pf,args[i]);
+        e = mk_app(e, args[i]);
+        auto p = m_app_builder.mk_app(get_congr_fun_name(), pf, args[i]);
         if (p) pf = *p;
-        else throw blast_exception("failed on [congr_fun] matching",e);
+        else throw blast_exception("failed on [congr_fun] matching", e);
     }
-    return result(e,pf);
+    return result(e, pf);
 }
 
 result simplifier::try_congrs(expr const & e) {
@@ -539,66 +534,65 @@ result simplifier::try_congrs(expr const & e) {
     if (!crs) return result(e);
 
     result r(e);
-    for_each(*crs,[&](congr_rule const & cr) {
+    for_each(*crs, [&](congr_rule const & cr) {
             if (!r.is_none()) return;
-            r = try_congr(e,cr);
-        }); 
+            r = try_congr(e, cr);
+        });
     return r;
 }
 
 result simplifier::try_congr(expr const & e, congr_rule const & cr) {
-    blast_tmp_type_context tmp_tctx(cr.get_num_umeta(),cr.get_num_emeta());
+    blast_tmp_type_context tmp_tctx(cr.get_num_umeta(), cr.get_num_emeta());
 
-    if (!tmp_tctx->is_def_eq(e,cr.get_lhs())) return result(e);
+    if (!tmp_tctx->is_def_eq(e, cr.get_lhs())) return result(e);
 
     if (m_trace) {
-        ios().get_diagnostic_channel() << "<" << cr.get_id() << "> " 
+        ios().get_diagnostic_channel() << "<" << cr.get_id() << "> "
                                        << e << " === " << cr.get_lhs() << "\n";
     }
-    
+
     /* First, iterate over the congruence hypotheses */
     bool failed = false;
     bool simplified = false;
     list<expr> const & congr_hyps = cr.get_congr_hyps();
-    for_each(congr_hyps,[&](expr const & m) {
+    for_each(congr_hyps, [&](expr const & m) {
         if (failed) return;
         buffer<expr> ls;
         expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
 
         while (is_pi(m_type)) {
             expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data());
-            expr l = tmp_tctx->mk_tmp_local(d,binding_info(m_type));
+            expr l = tmp_tctx->mk_tmp_local(d, binding_info(m_type));
             ls.push_back(l);
-            m_type = instantiate(binding_body(m_type),l);
+            m_type = instantiate(binding_body(m_type), l);
         }
 
         expr h_rel, h_lhs, h_rhs;
         bool valid = is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel);
         lean_assert(valid);
         {
-            simplify_caches fresh_caches;            
-            flet<simplify_caches> set_simplify_caches(m_simplify_caches,fresh_caches);            
-            flet<name> set_name(m_rel,const_name(h_rel));
-            
-            flet<simp_rule_sets> set_ctx_srss(m_ctx_srss,add_to_srss(m_ctx_srss,ls));
-            
+            simplify_caches fresh_caches;
+            flet<simplify_caches> set_simplify_caches(m_simplify_caches, fresh_caches);
+            flet<name> set_name(m_rel, const_name(h_rel));
+
+            flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls));
+
             h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
             result r_congr_hyp = simplify(h_lhs);
             expr hyp;
             if (r_congr_hyp.is_none()) {
                 hyp = finalize(r_congr_hyp).get_proof();
-            }
-            else {
+            } else {
                 hyp = r_congr_hyp.get_proof();
                 simplified = true;
             }
 
-            if (!tmp_tctx->is_def_eq(m,Fun(ls,hyp))) failed = true;
+            if (!tmp_tctx->is_def_eq(m, Fun(ls, hyp))) failed = true;
         }
         });
-    
+
     if (failed || !simplified) return result(e);
-    
+
     /* Traverse metavariables backwards, proving or synthesizing the rest */
     for (int i = cr.get_num_emeta() - 1; i >= 0; --i) {
         expr const & m = cr.get_emeta(i);
@@ -617,7 +611,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
         if (tmp_tctx->is_mvar_assigned(i)) continue;
 
         if (tmp_tctx->is_prop(tmp_tctx->infer(m))) {
-            // TODO try to prove
+            // TODO(dhs): should I try to prove?
             return result(e);
         }
 
@@ -636,7 +630,7 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
 
     expr e_s = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
     expr pf = tmp_tctx->instantiate_uvars_mvars(cr.get_proof());
-    return result(e_s,pf);
+    return result(e_s, pf);
 }
 
 /* Setup and teardown */
@@ -648,30 +642,22 @@ void initialize_simplifier() {
     g_simplify_memoize       = new name{"simplify", "memoize"};
     g_simplify_contextual    = new name{"simplify", "contextual"};
     g_simplify_expand_macros = new name{"simplify", "expand_macros"};
-    g_simplify_trace         = new name{"simplify", "trace"};    
+    g_simplify_trace         = new name{"simplify", "trace"};
 
     register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS,
                              "(simplify) max allowed steps in simplification");
-
     register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN,
                          "(simplify) use top-down rewriting instead of bottom-up");
-
     register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE,
                          "(simplify) rewrite exhaustively");
-
     register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE,
                          "(simplify) memoize simplifications");
-
     register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL,
                          "(simplify) use contextual simplification");
-
     register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS,
                          "(simplify) expand macros");
-
     register_bool_option(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE,
                          "(simplify) trace");
-    
-
 }
 
 void finalize_simplifier() {
@@ -680,14 +666,14 @@ void finalize_simplifier() {
     delete g_simplify_contextual;
     delete g_simplify_memoize;
     delete g_simplify_exhaustive;
-    delete g_simplify_top_down;    
+    delete g_simplify_top_down;
     delete g_simplify_max_steps;
 }
 
 /* Entry point */
 
 result simplify(branch const & b, name const & rel, expr const & e) {
-    return simplifier(b,rel)(e);
+    return simplifier(b, rel)(e);
 }
 
 }}
diff --git a/src/library/blast/simplifier.h b/src/library/blast/simplifier.h
index ac42933927..bdec7cd3fd 100644
--- a/src/library/blast/simplifier.h
+++ b/src/library/blast/simplifier.h
@@ -29,7 +29,6 @@ public:
 
     /* The following assumes that [e] and [m_new] are definitionally equal */
     void update(expr const & e) { m_new = e; }
-        
 };
 
 }
diff --git a/src/library/simplifier/simp_rule_set.cpp b/src/library/simplifier/simp_rule_set.cpp
index 624f1a9333..f67fc7a141 100644
--- a/src/library/simplifier/simp_rule_set.cpp
+++ b/src/library/simplifier/simp_rule_set.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/relation_manager.h"
 #include "library/simplifier/ceqv.h"
 #include "library/simplifier/simp_rule_set.h"
+#include <vector>
 
 namespace lean {
 simp_rule_core::simp_rule_core(name const & id, levels const & umetas, std::vector<expr> const & emetas,
@@ -44,7 +45,7 @@ format simp_rule::pp(formatter const & fmt) const {
 congr_rule::congr_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
                        std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
                        list<expr> const & congr_hyps):
-    simp_rule_core(id, umetas, emetas, instances, lhs, rhs, proof),    
+    simp_rule_core(id, umetas, emetas, instances, lhs, rhs, proof),
     m_congr_hyps(congr_hyps) {}
 
 bool operator==(congr_rule const & r1, congr_rule const & r2) {
@@ -265,13 +266,13 @@ simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s,
         expr proof = tctx.whnf(p.second);
         bool is_perm = is_permutation_ceqv(env, rule);
         std::vector<expr> emetas;
-        std::vector<bool> instances;        
+        std::vector<bool> instances;
         while (is_pi(rule)) {
             expr mvar = tctx.mk_mvar(binding_domain(rule));
             emetas.push_back(mvar);
             instances.push_back(binding_info(rule).is_inst_implicit());
             rule = tctx.whnf(instantiate(binding_body(rule), mvar));
-            proof = mk_app(proof,mvar);
+            proof = mk_app(proof, mvar);
         }
         expr rel, lhs, rhs;
         if (is_simp_relation(env, rule, rel, lhs, rhs) && is_constant(rel)) {
@@ -365,15 +366,15 @@ void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n)
     expr proof   = mk_constant(n, ls);
 
     std::vector<expr> emetas;
-    std::vector<bool> instances, explicits;        
-    
+    std::vector<bool> instances, explicits;
+
     while (is_pi(rule)) {
         expr mvar = tctx.mk_mvar(binding_domain(rule));
         emetas.push_back(mvar);
         explicits.push_back(is_explicit(binding_info(rule)));
         instances.push_back(binding_info(rule).is_inst_implicit());
         rule = tctx.whnf(instantiate(binding_body(rule), mvar));
-        proof = mk_app(proof,mvar);
+        proof = mk_app(proof, mvar);
     }
     expr rel, lhs, rhs;
     if (!is_simp_relation(tctx.env(), rule, rel, lhs, rhs) || !is_constant(rel)) {
@@ -455,7 +456,6 @@ void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n)
             congr_hyps.push_back(mvar);
         }
     }
-    
     s.insert(const_name(rel), congr_rule(n, ls, emetas, instances, lhs, rhs, proof, to_list(congr_hyps)));
 }
 
@@ -465,14 +465,14 @@ struct rrs_state {
     name_set                 m_congr_names;
 
     void add_simp(environment const & env, io_state const & ios, name const & cname) {
-        tmp_type_context tctx{env,ios};
+        tmp_type_context tctx{env, ios};
         m_sets = add_core(tctx, m_sets, cname);
         m_simp_names.insert(cname);
     }
 
     void add_congr(environment const & env, io_state const & ios, name const & n) {
-        tmp_type_context tctx{env,ios};        
-        add_congr_core(tctx,m_sets, n);
+        tmp_type_context tctx{env, ios};
+        add_congr_core(tctx, m_sets, n);
         m_congr_names.insert(n);
     }
 };
@@ -530,7 +530,7 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios,
     simp_rule_sets set;
     list<pair<bool, name>> const * cnames = rrs_ext::get_entries(env, ns);
     if (cnames) {
-        tmp_type_context tctx(env,ios);
+        tmp_type_context tctx(env, ios);
         for (pair<bool, name> const & p : *cnames) {
             set = add_core(tctx, set, p.second);
         }
diff --git a/src/library/simplifier/simp_rule_set.h b/src/library/simplifier/simp_rule_set.h
index 4d093ece66..511292a223 100644
--- a/src/library/simplifier/simp_rule_set.h
+++ b/src/library/simplifier/simp_rule_set.h
@@ -19,7 +19,7 @@ protected:
     levels              m_umetas;
     std::vector<expr>   m_emetas;
     std::vector<bool>   m_instances;
-    
+
     expr                m_lhs;
     expr                m_rhs;
     expr                m_proof;
@@ -32,7 +32,7 @@ public:
 
     expr const & get_emeta(unsigned i) const { return m_emetas[i]; }
     bool is_instance(unsigned i) const { return m_instances[i]; }
-    
+
     expr const & get_lhs() const { return m_lhs; }
     expr const & get_rhs() const { return m_rhs; }
     expr const & get_proof() const { return m_proof; }
@@ -59,7 +59,7 @@ class congr_rule : public simp_rule_core {
                std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
                list<expr> const & congr_hyps);
     friend void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n);
-public:    
+public:
     friend bool operator==(congr_rule const & r1, congr_rule const & r2);
     list<expr> const & get_congr_hyps() const { return m_congr_hyps; }
     format pp(formatter const & fmt) const;