diff --git a/src/frontends/lean/coercion_elaborator.cpp b/src/frontends/lean/coercion_elaborator.cpp
index 656f2e011..e35f376f3 100644
--- a/src/frontends/lean/coercion_elaborator.cpp
+++ b/src/frontends/lean/coercion_elaborator.cpp
@@ -17,7 +17,8 @@ coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr cons
                                          list<constraints> const & choices, list<expr> const & coes,
                                          bool use_id):
     m_info(info), m_arg(arg), m_id(use_id), m_choices(choices), m_coercions(coes) {
-    lean_assert(length(m_coercions) + 1 == length(m_choices));
+    lean_assert(!use_id || length(m_coercions) + 1 == length(m_choices));
+    lean_assert(use_id  || length(m_coercions)     == length(m_choices));
 }
 
 optional<constraints> coercion_elaborator::next() {
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index edc22b145..364ada4f2 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -419,8 +419,8 @@ public:
                 lean_assert(is_meta(f));
                 // let type checker add constraint
                 f_type = infer_type(f, cs);
-                lean_assert(is_pi(f_type));
                 f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
+                lean_assert(is_pi(f_type));
             }
         } else {
             erase_coercion_info(f);