diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 51b871605e..689f5c295e 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1903,7 +1903,7 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
         unsigned i       = 0;
         while (is_pi(proj_type)) {
             if (is_explicit(binding_info(proj_type))) {
-                if (is_app_of(binding_domain(proj_type), field_res.m_base_S_name)) {
+                if (is_app_of(extract_mdata(binding_domain(proj_type)), field_res.m_base_S_name)) {
                     /* found s location */
                     expr coerced_s = *mk_base_projections(m_env, field_res.m_S_name, field_res.m_base_S_name, mk_as_is(s));
                     new_args.push_back(copy_pos(fn, std::move(coerced_s)));
diff --git a/src/library/util.cpp b/src/library/util.cpp
index b7a9285d78..c69808ec0a 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -1030,6 +1030,14 @@ expr mk_tactic_unit() {
 static std::string * g_version_string = nullptr;
 std::string const & get_version_string() { return *g_version_string; }
 
+expr const & extract_mdata(expr const & e) {
+    if (is_mdata(e)) {
+        return extract_mdata(mdata_expr(e));
+    } else {
+        return e;
+    }
+}
+
 void initialize_library_util() {
     g_unit           = new expr(mk_constant(get_unit_name()));
     g_unit_mk        = new expr(mk_constant(get_unit_star_name()));
diff --git a/src/library/util.h b/src/library/util.h
index f2d77151b4..3058d44363 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -315,6 +315,8 @@ expr mk_tactic_unit();
 
 std::string const & get_version_string();
 
+expr const & extract_mdata(expr const &);
+
 void initialize_library_util();
 void finalize_library_util();
 }