diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp
index 8f6415c633..1f9f34aabb 100644
--- a/src/library/blast/simplifier.cpp
+++ b/src/library/blast/simplifier.cpp
@@ -24,7 +24,7 @@ Author: Daniel Selsam
 #include <map>
 
 #ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
-#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 100
+#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 1000
 #endif
 #ifndef LEAN_DEFAULT_SIMPLIFY_TOP_DOWN
 #define LEAN_DEFAULT_SIMPLIFY_TOP_DOWN false
@@ -339,7 +339,38 @@ result simplifier::simplify_app(expr const & e) {
 
     /* (2) Synthesize congruence lemma */
     if (using_eq()) {
-        // TODO(dhs): synthesize congruence lemma
+        buffer<expr> args;
+        expr fn = get_app_args(e, args);
+        if (auto congr_lemma = mk_congr_lemma_for_simp(fn, args.size())) {
+            expr proof = congr_lemma->get_proof();
+            expr type = congr_lemma->get_type();
+            unsigned i = 0;
+            bool simplified = false;
+            buffer<expr> locals;
+            for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
+                    proof = mk_app(proof, args[i]);
+                    type = instantiate(binding_body(type), args[i]);
+
+                    if (ckind == congr_arg_kind::Eq) {
+                        result r_arg = simplify(args[i]);
+                        if (!r_arg.is_none()) simplified = true;
+                        r_arg = finalize(r_arg);
+                        proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
+                        type = instantiate(binding_body(type), r_arg.get_new());
+                        type = instantiate(binding_body(type), r_arg.get_proof());
+                    }
+                    i++;
+                });
+            if (simplified) {
+                lean_assert(is_eq(type));
+                buffer<expr> type_args;
+                get_app_args(type, type_args);
+                expr & new_e = type_args[2];
+                return join(result(new_e, proof), simplify_fun(new_e));
+            } else {
+                return simplify_fun(e);
+            }
+        }
     }
 
     /* (3) Fall back on generic binary congruence */
diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp
index bedb9ad99f..18aeab2878 100644
--- a/src/library/congr_lemma_manager.cpp
+++ b/src/library/congr_lemma_manager.cpp
@@ -18,7 +18,7 @@ class congr_lemma_manager::imp {
     type_context &     m_ctx;
     bool               m_ignore_inst_implicit;
     struct key {
-        expr const & m_fn;
+        expr         m_fn;
         unsigned     m_nargs;
         unsigned     m_hash;
         key(expr const & fn, unsigned nargs):
diff --git a/tests/lean/simplifier13.lean b/tests/lean/simplifier13.lean
new file mode 100644
index 0000000000..fd79be4db7
--- /dev/null
+++ b/tests/lean/simplifier13.lean
@@ -0,0 +1,10 @@
+universe l
+constants (T : Type.{l}) (f : T →  T → T) (g : T → T) 
+constants (P : T → Prop) (Q : Prop) (Hfg : ∀ (x : T), f x x = g x)
+constants (c : Π (x y z : T), P x → P y → P z → Q) 
+constants (x y z : T) (px : P (f x x)) (py : P (f y y)) (pz : P (g z))
+
+attribute Hfg [simp]
+
+#simplify eq 0 c (f x x) (f y y) (g z) px py pz
+
diff --git a/tests/lean/simplifier13.lean.expected.out b/tests/lean/simplifier13.lean.expected.out
new file mode 100644
index 0000000000..279c5cb077
--- /dev/null
+++ b/tests/lean/simplifier13.lean.expected.out
@@ -0,0 +1 @@
+c (g x) (g y) (g z) (eq.rec px (Hfg x)) (eq.rec py (Hfg y)) (eq.rec pz (eq.refl (g z)))
diff --git a/tests/lean/simplifier3.lean b/tests/lean/simplifier3.lean
index 83e57752cc..e0afe33741 100644
--- a/tests/lean/simplifier3.lean
+++ b/tests/lean/simplifier3.lean
@@ -13,7 +13,7 @@ attribute Hgyhz [simp]
 attribute Hab [simp]
 attribute Hbc [simp]
 
-#simplify eq 2 (f x a) -- h z c
+#simplify eq 2 (f x a)
 
 end test_congr
 
diff --git a/tests/lean/simplifier3.lean.expected.out b/tests/lean/simplifier3.lean.expected.out
index ea10d9d832..9b1cfda9f7 100644
--- a/tests/lean/simplifier3.lean.expected.out
+++ b/tests/lean/simplifier3.lean.expected.out
@@ -1,2 +1,2 @@
-f x a = h z c
+f x a = f x c
 f x = g x
diff --git a/tests/lean/simplifier7.lean b/tests/lean/simplifier7.lean
index ef94541b0d..549a3f07ad 100644
--- a/tests/lean/simplifier7.lean
+++ b/tests/lean/simplifier7.lean
@@ -11,5 +11,6 @@ attribute H3 [simp]
 attribute Hf [simp]
 attribute Hg [simp]
 
+
 #simplify iff 2 (and P1 (and P2 P3))
 #simplify iff 2 (and P1 (iff P2 P3))