diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 01ef9d7385..693361cc7f 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2876,18 +2876,14 @@ class visit_structure_instance_fn {
     name_map<expr> m_field2mvar;
     name_map<name> m_mvar2field;
 
-    void insert_field_preterm(name const & S_fname, expr const & p) {
-        m_field2elab.insert(S_fname, [=](expr const & d) {
-            return m_elab.visit(p, some_expr(d));
-        });
-    }
-
     bool field_from_source(name const & S_fname) {
         for (source const & src : m_sources) {
             if (optional<name> base_S_name = find_field(m_env, src.m_S_name, S_fname)) {
                 expr base_src = *mk_base_projections(m_env, src.m_S_name, *base_S_name, src.m_e);
                 expr f = mk_proj_app(m_env, *base_S_name, S_fname, base_src);
-                insert_field_preterm(S_fname, f);
+                m_field2elab.insert(S_fname, [=](expr const & d) {
+                    return m_elab.visit(f, some_expr(d));
+                });
                 return true;
             }
         }
@@ -2983,7 +2979,10 @@ class visit_structure_instance_fn {
                 if (it != m_fnames.end()) {
                     /* explicitly passed field */
                     m_fnames_used.insert(S_fname);
-                    insert_field_preterm(S_fname, m_fvalues[it - m_fnames.begin()]);
+                    const expr & p = m_fvalues[it - m_fnames.begin()];
+                    m_field2elab.insert(S_fname, [=](expr const & d) {
+                        return m_elab.visit(p, some_expr(consume_auto_opt_param(d)));
+                    });
                 } else if (auto p = is_subobject_field(m_env, nested_S_name, S_fname)) {
                     /* subobject field */
                     auto num_used = m_fnames_used.size();
diff --git a/src/library/congr_lemma.cpp b/src/library/congr_lemma.cpp
index 7e68fcb6cf..e973693b2e 100644
--- a/src/library/congr_lemma.cpp
+++ b/src/library/congr_lemma.cpp
@@ -525,8 +525,8 @@ struct congr_lemma_manager {
                 expr rhs = locals.push_local(binding_name(fn_type_rhs).append_after("'"), binding_domain(fn_type_rhs));
                 rhss.push_back(rhs); hyps.push_back(rhs);
                 expr eq_type;
-                expr domain_lhs = consume_opt_param(binding_domain(fn_type_lhs));
-                expr domain_rhs = consume_opt_param(binding_domain(fn_type_rhs));
+                expr domain_lhs = consume_auto_opt_param(binding_domain(fn_type_lhs));
+                expr domain_rhs = consume_auto_opt_param(binding_domain(fn_type_rhs));
                 if (domain_lhs == domain_rhs) {
                     eq_type = mk_eq(m_ctx, lhs, rhs);
                     kinds.push_back(congr_arg_kind::Eq);
diff --git a/src/library/fun_info.cpp b/src/library/fun_info.cpp
index 45e8c775ed..17c2b7aabf 100644
--- a/src/library/fun_info.cpp
+++ b/src/library/fun_info.cpp
@@ -98,7 +98,7 @@ static list<unsigned> get_core(type_context & ctx,
     while (is_pi(type)) {
         if (i == max_args)
             break;
-        expr local_type = consume_opt_param(binding_domain(type));
+        expr local_type = consume_auto_opt_param(binding_domain(type));
         expr local      = locals.push_local(binding_name(type), local_type, binding_info(type));
         expr new_type   = ctx.relaxed_try_to_pi(instantiate(binding_body(type), local));
         bool is_prop    = ctx.is_prop(local_type);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index a30697ca32..2a5244f6db 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -105,9 +105,8 @@ bool is_app_of(expr const & t, name const & f_name, unsigned nargs) {
     return is_constant(fn) && const_name(fn) == f_name && get_app_num_args(t) == nargs;
 }
 
-expr consume_opt_param(expr const & type) {
-    if (is_app_of(type, get_opt_param_name(), 2)) {
-        /* make sure (opt_param 'a value) does not affect results */
+expr consume_auto_opt_param(expr const & type) {
+    if (is_app_of(type, get_auto_param_name(), 2) || is_app_of(type, get_opt_param_name(), 2)) {
         return app_arg(app_fn(type));
     } else {
         return type;
diff --git a/src/library/util.h b/src/library/util.h
index f37022ffd8..92562099fe 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -43,8 +43,8 @@ bool is_app_of(expr const & t, name const & f_name);
 /** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_nargs) */
 bool is_app_of(expr const & t, name const & f_name, unsigned nargs);
 
-/** \brief If type is of the form (opt_param A v), return A. Otherwise, return type. */
-expr consume_opt_param(expr const & type);
+/** \brief If type is of the form (auto_param A p) or (opt_param A v), return A. Otherwise, return type. */
+expr consume_auto_opt_param(expr const & type);
 
 /** \brief Unfold constant \c e or constant application (i.e., \c e is of the form (f ....),
     where \c f is a constant */