diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 8bda9e508..c699c873c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -52,6 +52,7 @@ static format * g_let_fmt         = nullptr;
 static format * g_in_fmt          = nullptr;
 static format * g_assign_fmt      = nullptr;
 static format * g_have_fmt        = nullptr;
+static format * g_assert_fmt      = nullptr;
 static format * g_from_fmt        = nullptr;
 static format * g_visible_fmt     = nullptr;
 static format * g_show_fmt        = nullptr;
@@ -127,6 +128,7 @@ void initialize_pp() {
     g_in_fmt          = new format(highlight_keyword(format("in")));
     g_assign_fmt      = new format(highlight_keyword(format(":=")));
     g_have_fmt        = new format(highlight_keyword(format("have")));
+    g_assert_fmt      = new format(highlight_keyword(format("assert")));
     g_from_fmt        = new format(highlight_keyword(format("from")));
     g_visible_fmt     = new format(highlight_keyword(format("[visible]")));
     g_show_fmt        = new format(highlight_keyword(format("show")));
@@ -152,6 +154,7 @@ void finalize_pp() {
     delete g_in_fmt;
     delete g_assign_fmt;
     delete g_have_fmt;
+    delete g_assert_fmt;
     delete g_from_fmt;
     delete g_visible_fmt;
     delete g_show_fmt;
@@ -638,9 +641,8 @@ auto pretty_fn::pp_have(expr const & e) -> result {
     format type_fmt  = pp_child(mlocal_type(local), 0).fmt();
     format proof_fmt = pp_child(proof, 0).fmt();
     format body_fmt  = pp_child(body, 0).fmt();
-    format r = *g_have_fmt + space() + format(n) + space();
-    if (binding_info(binding).is_contextual())
-        r += compose(*g_visible_fmt, space());
+    format head_fmt  = (binding_info(binding).is_contextual()) ? *g_assert_fmt : *g_have_fmt;
+    format r = head_fmt + space() + format(n) + space();
     r += colon() + nest(m_indent, line() + type_fmt + comma() + space() + *g_from_fmt);
     r = group(r);
     r += nest(m_indent, line() + proof_fmt + comma());
diff --git a/src/library/pp_options.cpp b/src/library/pp_options.cpp
index 45cb76793..7921dc036 100644
--- a/src/library/pp_options.cpp
+++ b/src/library/pp_options.cpp
@@ -8,11 +8,11 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
-#define LEAN_DEFAULT_PP_MAX_DEPTH 100
+#define LEAN_DEFAULT_PP_MAX_DEPTH 10000
 #endif
 
 #ifndef LEAN_DEFAULT_PP_MAX_STEPS
-#define LEAN_DEFAULT_PP_MAX_STEPS 500
+#define LEAN_DEFAULT_PP_MAX_STEPS 50000
 #endif
 
 #ifndef LEAN_DEFAULT_PP_NOTATION