diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 4e4dea7d9..275b252fe 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -248,7 +248,7 @@ class pp_fn {
         if (has_implicit_arguments(v.get_name())) {
             return mk_result(format(m_frontend.get_explicit_version(v.get_name())), 1);
         } else {
-            return mk_result(v.pp(m_unicode), 1);
+            return mk_result(v.pp(m_unicode, m_coercion), 1);
         }
     }
 
@@ -699,7 +699,7 @@ class pp_fn {
             if (is_constant(f))
                 p = mk_result(format(const_name(f)), 1);
             else if (is_value(f))
-                p = mk_result(to_value(f).pp(m_unicode), 1);
+                p = mk_result(to_value(f).pp(m_unicode, m_coercion), 1);
             else
                 p = pp_child(f, depth);
             bool simple     = is_constant(f) && const_name(f).size() <= m_indent + 4;
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index dfc7ece40..5298ee8a7 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -127,7 +127,7 @@ bool value::operator<(value const & other) const {
         return get_name() < other.get_name();
 }
 format value::pp() const { return format(get_name()); }
-format value::pp(bool unicode) const { return unicode ? format(get_unicode_name()) : pp(); }
+format value::pp(bool unicode, bool) const { return unicode ? format(get_unicode_name()) : pp(); }
 unsigned value::hash() const { return get_name().hash(); }
 expr_value::expr_value(value & v):
     expr_cell(expr_kind::Value, v.hash(), false),
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index ee991067c..a70f14b19 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -244,7 +244,7 @@ public:
     bool operator<(value const & other) const;
     virtual void display(std::ostream & out) const;
     virtual format pp() const;
-    virtual format pp(bool unicode) const;
+    virtual format pp(bool unicode, bool coercion) const;
     virtual unsigned hash() const;
 };
 /** \brief Semantic attachments */
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
index 6272c93ac..b83243bef 100644
--- a/src/library/arith/int.cpp
+++ b/src/library/arith/int.cpp
@@ -37,8 +37,13 @@ public:
         return _other && _other->m_val == m_val;
     }
     virtual void display(std::ostream & out) const { out << m_val; }
-    virtual format pp() const { return format(m_val); }
-    virtual format pp(bool ) const { return pp(); }
+    virtual format pp() const { return pp(false, false); }
+    virtual format pp(bool unicode, bool coercion) const {
+        if (coercion)
+            return format{to_value(mk_nat_to_int_fn()).pp(unicode, coercion), space(), format(m_val)};
+        else
+            return format(m_val);
+    }
     virtual unsigned hash() const { return m_val.hash(); }
     mpz const & get_num() const { return m_val; }
 };
diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp
index 8a3be0081..8d172a5c2 100644
--- a/src/library/arith/nat.cpp
+++ b/src/library/arith/nat.cpp
@@ -37,7 +37,7 @@ public:
     }
     virtual void display(std::ostream & out) const { out << m_val; }
     virtual format pp() const { return format(m_val); }
-    virtual format pp(bool ) const { return pp(); }
+    virtual format pp(bool, bool) const { return pp(); }
     virtual unsigned hash() const { return m_val.hash(); }
     mpz const & get_num() const { return m_val; }
 };
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
index cc94fbe65..fd0c3182f 100644
--- a/src/library/arith/real.cpp
+++ b/src/library/arith/real.cpp
@@ -40,8 +40,13 @@ public:
         return _other && _other->m_val == m_val;
     }
     virtual void display(std::ostream & out) const { out << m_val; }
-    virtual format pp() const { return format(m_val); }
-    virtual format pp(bool ) const { return pp(); }
+    virtual format pp() const { return pp(false, false); }
+    virtual format pp(bool, bool coercion) const {
+        if (coercion)
+            return format{format(const_name(mk_nat_to_real_fn())), space(), format(m_val)};
+        else
+            return format(m_val);
+    }
     virtual unsigned hash() const { return m_val.hash(); }
     mpq const & get_num() const { return m_val; }
 };
diff --git a/tests/lean/subst.lean.expected.out b/tests/lean/subst.lean.expected.out
index 8c36261b2..c377c8af2 100644
--- a/tests/lean/subst.lean.expected.out
+++ b/tests/lean/subst.lean.expected.out
@@ -9,4 +9,4 @@
   Set: lean::pp::notation
   Set: lean::pp::implicit
 Theorem T : eq::explicit ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) :=
-    Subst::explicit ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == 10) H1 H2
+    Subst::explicit ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == nat_to_int 10) H1 H2