diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e8d4cfca54..f688f29279 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -823,7 +823,7 @@ public:
         expr a_type = instantiate_metavars(infer_type(a));
         expr r      = mk_app(f, a, e.get_tag());
 
-        justification j = mk_app_justification(e, a, d_type, a_type);
+        justification j = mk_app_justification(r, a, d_type, a_type);
         expr new_a  = ensure_type(a, a_type, d_type, j, m_relax_main_opaque);
         return update_app(r, app_fn(r), new_a);
     }
@@ -1205,7 +1205,7 @@ public:
         flet<bool> set_relax(m_relax_main_opaque, is_opaque && !get_hide_main_opaque(m_env));
         expr r_v      = visit(v);
         expr r_v_type = infer_type(r_v);
-        justification j = mk_justification(v, [=](formatter const & fmt, substitution const & subst) {
+        justification j = mk_justification(r_v, [=](formatter const & fmt, substitution const & subst) {
                 substitution s(subst);
                 return pp_def_type_mismatch(fmt, n, s.instantiate(r_t), s.instantiate(r_v_type));
             });
diff --git a/tests/lean/calc1.lean.expected.out b/tests/lean/calc1.lean.expected.out
index 3dc100662c..e18623b03c 100644
--- a/tests/lean/calc1.lean.expected.out
+++ b/tests/lean/calc1.lean.expected.out
@@ -1,4 +1,4 @@
 le_eq_trans a d e (le_trans a c d (eq_le_trans a b c H1 H2) H3) H4 : le a e
 calc1.lean:38:10: error: invalid 'calc' expression, transitivity rule is not defined for current step
 le_lt_trans b c d H2 H5 : lt b d
-[choice ([@ le2_trans] b d e ([@ le2_trans] b c d H2 H3) H4) ([@ le_trans] b d e ([@ le_trans] b c d H2 H3) H4)]
+[choice (@le2_trans b d e (@le2_trans b c d H2 H3) H4) (@le_trans b d e (@le_trans b c d H2 H3) H4)]
diff --git a/tests/lean/crash.lean.expected.out b/tests/lean/crash.lean.expected.out
index fd683ab40f..a4b7b68b35 100644
--- a/tests/lean/crash.lean.expected.out
+++ b/tests/lean/crash.lean.expected.out
@@ -1,6 +1,6 @@
 crash.lean:8:12: error: type mismatch at application
   have H' : not P, from H,
-  _
+  ?M_1 P H
 term
   H
 is expected of type