diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 0a922bb1c1..d2089c5cd9 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -443,12 +443,14 @@ optional<expr> elaborator::mk_coercion(expr const & e, expr const & _e_type, exp
     }
 }
 
-optional<expr> elaborator::ensure_has_type(expr const & e, expr const & e_type, expr const & type, expr const & ref) {
+bool elaborator::is_def_eq(expr const & e1, expr const & e2) {
     type_context::approximate_scope scope(m_ctx);
+    return m_ctx.is_def_eq(e1, e2);
+}
 
+optional<expr> elaborator::ensure_has_type(expr const & e, expr const & e_type, expr const & type, expr const & ref) {
     if (is_def_eq(e_type, type))
         return some_expr(e);
-
     return mk_coercion(e, e_type, type, ref);
 }
 
@@ -1800,7 +1802,8 @@ expr elaborator::visit_suffices_expr(expr const & e, optional<expr> const & expe
 
 expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
     flet<unsigned> inc_depth(m_depth, m_depth+1);
-    trace_elab_detail(tout() << "[" << m_depth << "] visiting\n" << e << "\n";);
+    trace_elab_detail(tout() << "[" << m_depth << "] visiting\n" << e << "\n";
+                      if (expected_type) tout() << "expected type:\n" << instantiate_mvars(*expected_type) << "\n";);
     if (is_placeholder(e)) {
         return visit_placeholder(e, expected_type);
     } else if (is_have_expr(e)) {
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 86408c08f1..1826b45a2a 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -99,7 +99,7 @@ private:
 
     expr whnf(expr const & e) { return m_ctx.whnf(e); }
     expr try_to_pi(expr const & e) { return m_ctx.try_to_pi(e); }
-    bool is_def_eq(expr const & e1, expr const & e2) { return m_ctx.is_def_eq(e1, e2); }
+    bool is_def_eq(expr const & e1, expr const & e2);
     bool assign_mvar(expr const & e1, expr const & e2) { lean_assert(is_metavar(e1)); return is_def_eq(e1, e2); }
     expr instantiate_mvars(expr const & e);
     bool is_uvar_assigned(level const & l) const { return m_ctx.is_assigned(l); }
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 60eda14df4..7d23234869 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2276,7 +2276,7 @@ bool type_context::is_def_eq(expr const & t, expr const & s) {
     bool success = is_def_eq_core(t, s);
     lean_trace(name({"type_context", "is_def_eq"}),
                tout() << t << " =?= " << s << " ... "
-               << (success ? "success" : "failed") << "\n";);
+               << (success ? "success" : "failed") << " " << (approximate() ? " (approximate mode)" : "") << "\n";);
     if (success) {
         S.commit();
         return true;