diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index 13e3de263..db6bd41af 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -123,7 +123,7 @@ class frontend_elaborator::imp {
 
         virtual expr visit_constant(expr const & e, context const & ctx) {
             if (is_placeholder(e)) {
-                expr m = m_ref.m_menv.mk_metavar(ctx, const_type(e));
+                expr m = m_ref.m_menv.mk_metavar(ctx, visit(const_type(e), ctx));
                 m_ref.m_trace[m] = e;
                 return m;
             } else {
diff --git a/tests/lean/tactic14.lean b/tests/lean/tactic14.lean
new file mode 100644
index 000000000..9d7eb5de4
--- /dev/null
+++ b/tests/lean/tactic14.lean
@@ -0,0 +1,12 @@
+(**
+
+-- Tactic for trying to prove goal using Reflexivity, Congruence and available assumptions
+congr_tac = TRY(unfold_tac("eq")) ..REPEAT(ORELSE(apply_tac("Refl"), apply_tac("Congr"), assumption_tac))
+
+**)
+
+Theorem T1 (a b : Int) (f : Int -> Int) : a = b -> (f (f a)) = (f (f b)) :=
+   fun assumption : a = b,
+      show (f (f a)) = (f (f b)) by congr_tac
+
+Show Environment 1.
diff --git a/tests/lean/tactic14.lean.expected.out b/tests/lean/tactic14.lean.expected.out
new file mode 100644
index 000000000..7d2bbaf73
--- /dev/null
+++ b/tests/lean/tactic14.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Proved: T1
+Theorem T1 (a b : ℤ) (f : ℤ → ℤ) (assumption : a = b) : (f (f a)) = (f (f b)) :=
+    Congr (Refl f) (Congr (Refl f) assumption)