diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 6736f9c273..bf6873445f 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1876,41 +1876,85 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
     } else if (is_field_notation(fn) && amask == arg_mask::Default) {
         expr s           = visit(macro_arg(fn, 0), none_expr());
         expr s_type      = head_beta_reduce(instantiate_mvars(infer_type(s)));
-        auto field_res   = find_field_fn(fn, s, s_type);
+        auto field_res   = resolve_field_notation(fn, s, s_type);
+
         expr proj, proj_type;
-        if (field_res.m_ldecl) {
-            proj      = copy_tag(fn, field_res.m_ldecl->mk_ref());
-            proj_type = field_res.m_ldecl->get_type();
-        } else {
-            proj      = copy_tag(fn, mk_constant(field_res.get_full_fname()));
-            proj_type = m_env.get(field_res.get_full_fname()).get_type();
+        switch (field_res.m_kind) {
+            case field_resolution::kind::ProjFn: {
+                // Projections are handled specially since `s` is inserted at a specific argument, whether
+                // or not it is explicit.
+                expr coerced_s = *mk_base_projections(m_env, field_res.get_struct_name(), field_res.get_base_struct_name(), mk_as_is(s));
+                expr proj_app = mk_proj_app(m_env, field_res.get_base_struct_name(), field_res.get_field_name(), coerced_s, fn);
+                expr new_proj = visit_function(proj_app, has_args, has_args ? none_expr() : expected_type, ref);
+                return visit_base_app(new_proj, arg_mask::Default, args, expected_type, ref);
+            }
+            case field_resolution::kind::LocalRec: {
+                s = mk_as_is(s);
+                proj = copy_tag(fn, field_res.m_ldecl.mk_ref());
+                proj_type = field_res.m_ldecl.get_type();
+                break;
+            }
+            case field_resolution::kind::Const: {
+                expr coerced_s = *mk_base_projections(m_env, field_res.get_struct_name(), field_res.get_base_struct_name(), mk_as_is(s));
+                s = copy_tag(s, std::move(coerced_s));
+                proj = copy_tag(fn, mk_constant(field_res.get_const_name()));
+                proj_type = m_env.get(field_res.get_full_name()).get_type();
+                break;
+            }
+            default: lean_unreachable();
         }
+
+        expr new_proj = visit_function(proj, has_args, has_args ? none_expr() : expected_type, ref);
+
+        name base_name = field_res.get_base_struct_name();
         buffer<expr> new_args;
-        unsigned i       = 0;
+        optional<elaborator_exception> insufficient;
+        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(binding_domain(proj_type), base_name)
+                    || (is_pi(binding_domain(proj_type)) && base_name == get_function_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_tag(fn, std::move(coerced_s)));
+
+                    if (insufficient) {
+                        // We defer reporting this to here to prefer the "does not have explicit argument with type" error
+                        report_or_throw(*insufficient);
+                    }
+
+                    new_args.push_back(s);
                     for (; i < args.size(); i++)
                         new_args.push_back(args[i]);
-                    expr new_proj = visit_function(proj, has_args, has_args ? none_expr() : expected_type, ref);
-                    return visit_base_app(new_proj, amask, new_args, expected_type, ref);
-                } else {
-                    if (i >= args.size()) {
-                        throw elaborator_exception(ref, sstream() << "invalid field notation, insufficient number of arguments for '"
-                                                   << field_res.get_full_fname() << "'");
-                    }
+
+                    return visit_base_app(new_proj, arg_mask::Default, new_args, expected_type, ref);
+                } else if (i < args.size()) {
                     new_args.push_back(args[i]);
                     i++;
+                } else {
+                    if (!insufficient) {
+                        insufficient = elaborator_exception(ref, sstream() << "invalid field notation, insufficient number of arguments for '"
+                                                                    << field_res.get_full_name() << "'");
+                    }
+                    new_args.push_back(mk_sorry(none_expr(), fn));
                 }
             }
             proj_type = binding_body(proj_type);
         }
-        throw elaborator_exception(ref, sstream() << "invalid field notation, function '"
-                                   << field_res.get_full_fname() << "' does not have explicit argument with type ("
-                                   << field_res.m_base_S_name << " ...)");
+
+        // If there is no explicit argument of the right type, we try inserting it as the first explicit argument.
+        // This gives some ability to use dot notation with terms that have a `has_coe_to_fun` instance.
+
+        new_args.clear();
+        new_args.push_back(s);
+        new_args.append(args);
+
+        try {
+            return visit_base_app(new_proj, arg_mask::Default, new_args, expected_type, ref);
+        } catch (elaborator_exception & ex) {
+            throw nested_elaborator_exception(ref, ex, format("invalid field notation, function '")
+                                                + format(field_res.get_full_name())
+                                                + format("' does not have explicit argument with type (")
+                                                + format(field_res.get_base_struct_name()) + format(" ...)"));
+        }
     } else {
         expr new_fn = visit_function(fn, has_args, has_args ? none_expr() : expected_type, ref);
         /* Check if we should use a custom elaboration procedure for this application. */
@@ -2685,42 +2729,47 @@ expr elaborator::visit_inaccessible(expr const & e, optional<expr> const & expec
     return copy_tag(e, mk_inaccessible(new_a));
 }
 
-elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr const & s, expr const & s_type) {
-    // prefer 'unknown identifier' error when lhs is a constant of non-value type
-    if (is_field_notation(e)) {
-        auto lhs = macro_arg(e, 0);
-        if (is_constant(lhs)) {
-            type_context_old::tmp_locals locals(m_ctx);
-            expr t = whnf(s_type);
-            while (is_pi(t)) {
-                t = whnf(instantiate(binding_body(t), locals.push_local_from_binding(t)));
-            }
-            if (is_sort(t) && !is_anonymous_field_notation(e)) {
-                name fname = get_field_notation_field_name(e);
-                throw elaborator_exception(lhs, format("unknown identifier '") + format(const_name(lhs)) + format(".") +
-                                           format(fname) + format("'"));
-            }
+elaborator::field_resolution elaborator::resolve_field_notation_aux(expr const & e, expr const & s, expr const & s_type) {
+    lean_assert(is_field_notation(e));
+
+    // If it's a function, resolve the field as a declaration in the `function` namespace.
+    if (is_pi(s_type) && !is_anonymous_field_notation(e)) {
+        auto fname = get_field_notation_field_name(e);
+        auto full_fname = get_function_name() + fname;
+        if (m_env.find(full_fname)) {
+            return field_resolution_const(get_function_name(), get_function_name(), full_fname);
         }
     }
-    expr I      = get_app_fn(s_type);
+
+    expr I = get_app_fn(s_type);
+
     if (!is_constant(I)) {
         auto pp_fn = mk_pp_ctx();
+        // prefer 'unknown identifier' error when lhs (the unelaborated s) is a constant of non-value type
+        auto lhs = macro_arg(e, 0);
+        if (!is_anonymous_field_notation(e) && is_constant(lhs)) {
+            name fname = get_field_notation_field_name(e);
+            throw elaborator_exception(lhs, format("unknown identifier '") + format(const_name(lhs) + fname) + format("'"));
+        }
         throw elaborator_exception(e, format("invalid field notation, type is not of the form (C ...) where C is a constant") +
                                    pp_indent(pp_fn, s) +
                                    line() + format("has type") +
                                    pp_indent(pp_fn, s_type));
     }
+
+    auto struct_name = const_name(I);
+
     if (is_anonymous_field_notation(e)) {
-        if (!is_structure(m_env, const_name(I))) {
+        if (!is_structure(m_env, struct_name)) {
             auto pp_fn = mk_pp_ctx();
             throw elaborator_exception(e, format("invalid projection, structure expected") +
                                        pp_indent(pp_fn, s) +
                                        line() + format("has type") +
                                        pp_indent(pp_fn, s_type));
         }
-        auto fnames = get_structure_fields(m_env, const_name(I));
+        auto fnames = get_structure_fields(m_env, struct_name);
         unsigned fidx = get_field_notation_field_idx(e);
-        if (fidx  == 0) {
+        if (fidx == 0) {
             throw elaborator_exception(e, "invalid projection, index must be greater than 0");
         }
         if (fidx > fnames.size()) {
@@ -2731,37 +2780,46 @@ elaborator::field_resolution elaborator::field_to_decl(expr const & e, expr cons
                                        line() + format("which has type") +
                                        pp_indent(pp_fn, s_type));
         }
-        return const_name(I) + fnames[fidx-1];
+        return field_resolution_proj_fn(struct_name, struct_name, fnames[fidx-1]);
     } else {
-        name fname  = get_field_notation_field_name(e);
-        // search for "true" fields first, including in parent structures
-        if (is_structure_like(m_env, const_name(I)))
-            if (auto p = find_field(m_env, const_name(I), fname))
-                return field_resolution(const_name(I), *p, fname);
-        name full_fname = const_name(I) + fname;
-        name local_name = full_fname.replace_prefix(get_namespace(env()), {});
-        if (auto ldecl = m_ctx.lctx().find_if([&](local_decl const & decl) {
-            return decl.get_info().is_rec() && decl.get_pp_name() == local_name;
-        })) {
-            // projection is recursive call
-            return field_resolution(full_fname, ldecl);
+        name fname = get_field_notation_field_name(e);
+
+        // Search for "true" fields first, including in parent structures
+        if (is_structure_like(m_env, struct_name))
+            if (auto p = find_field(m_env, struct_name, fname))
+                return field_resolution_proj_fn(*p, struct_name, fname);
+
+        // Check if field notation is being used to make a "local" recursive call.
+        name full_fname = struct_name + fname;
+        name local_name = full_fname.replace_prefix(get_namespace(m_env), {});
+        if (auto ldecl = m_ctx.lctx().find_if([&](local_decl const & decl) { return decl.get_info().is_rec() && decl.get_pp_name() == local_name; })) {
+            return field_resolution_local_rec(struct_name, full_fname, *ldecl);
         }
-        if (!m_env.find(full_fname)) {
-            auto pp_fn = mk_pp_ctx();
-            throw elaborator_exception(e, format("invalid field notation, '") + format(fname) + format("'") +
-                                       format(" is not a valid \"field\" because environment does not contain ") +
-                                       format("'") + format(full_fname) + format("'") +
-                                       pp_indent(pp_fn, s) +
-                                       line() + format("which has type") +
-                                       pp_indent(pp_fn, s_type));
+
+        // Otherwise we search the environment for this "extended" dot notation
+
+        if (auto m = find_method(m_env, struct_name, fname)) {
+            return field_resolution_const(m->first, struct_name, m->second);
+        }
+
+        if (auto m = find_method_alias(m_env, struct_name, fname)) {
+            return field_resolution_const(m->first, m->first, m->second);
         }
-        return full_fname;
+
+        auto pp_fn = mk_pp_ctx();
+        throw elaborator_exception(e, format("invalid field notation, '") + format(fname) + format("'") +
+                                    format(" is not a valid \"field\" because environment does not contain ") +
+                                    format("'") + format(struct_name + fname) + format("'") +
+                                    pp_indent(pp_fn, s) +
+                                    line() + format("which has type") +
+                                    pp_indent(pp_fn, s_type));
     }
 }
 
-elaborator::field_resolution elaborator::find_field_fn(expr const & e, expr const & s, expr const & s_type) {
+elaborator::field_resolution elaborator::resolve_field_notation(expr const & e, expr const & s, expr const & s_type) {
+    lean_assert(is_field_notation(e));
     try {
-        return field_to_decl(e, s, s_type);
+        return resolve_field_notation_aux(e, s, s_type);
     } catch (elaborator_exception & ex1) {
         expr new_s_type = s_type;
         if (auto d = unfold_term(env(), new_s_type))
@@ -2770,7 +2828,7 @@ elaborator::field_resolution elaborator::find_field_fn(expr const & e, expr cons
         if (new_s_type == s_type)
             throw;
         try {
-            return find_field_fn(e, s, new_s_type);
+            return resolve_field_notation(e, s, new_s_type);
         } catch (elaborator_exception & ex2) {
             throw nested_elaborator_exception(ex2.get_pos(), ex1, ex2.pp());
         }
@@ -2779,17 +2837,7 @@ elaborator::field_resolution elaborator::find_field_fn(expr const & e, expr cons
 
 expr elaborator::visit_field(expr const & e, optional<expr> const & expected_type) {
     lean_assert(is_field_notation(e));
-    expr s         = visit(macro_arg(e, 0), none_expr());
-    expr s_type    = head_beta_reduce(instantiate_mvars(infer_type(s)));
-    auto field_res = find_field_fn(e, s, s_type);
-    expr proj_app;
-    if (field_res.m_ldecl) {
-        proj_app   = copy_tag(e, mk_app(field_res.m_ldecl->mk_ref(), mk_as_is(s)));
-    } else {
-        expr new_e = *mk_base_projections(m_env, field_res.m_S_name, field_res.m_base_S_name, mk_as_is(s));
-        proj_app   = mk_proj_app(m_env, field_res.m_base_S_name, field_res.m_fname, new_e, e);
-    }
-    return visit(proj_app, expected_type);
+    return visit_app_core(e, buffer<expr>(), expected_type, e);
 }
 
 class reduce_projections_visitor : public replace_visitor {
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 9d40de292c..9e685eab8e 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -246,23 +246,101 @@ class elaborator {
     expr visit_equation(expr const & eq, unsigned num_fns);
     expr visit_inaccessible(expr const & e, optional<expr> const & expected_type);
 
+    /** Field resolution: this is a field projection */
+    struct field_resolution_proj_fn {
+        /** Name of the structure that is the source of the field. Is ancestor of \c m_struct_name
+         * If this is not equal to \c m_struct_name then we should insert parent projections. */
+        name m_base_struct_name;
+        /** Name of the structure for the expression being projected. */
+        name m_struct_name;
+        /** The field name for the projection */
+        name m_field_name;
+
+        field_resolution_proj_fn(name const & base_struct_name, name const & struct_name, name const & field_name):
+            m_base_struct_name(base_struct_name), m_struct_name(struct_name), m_field_name(field_name) {}
+    };
+
+    /** Field resolution: this is a "method" (a.k.a. extended dot notation) */
+    struct field_resolution_const {
+        /** Name of the structure that is the source of the method. Is ancestor of \c m_struct_name
+         * If this is not equal to \c m_struct_name then we should insert parent projections. */
+        name m_base_struct_name;
+        /** Name of the generalized structure for the expression whose method is being called. */
+        name m_struct_name;
+        /** Name of the constant to use as a function */
+        name m_const_name;
+
+        field_resolution_const(name const & base_struct_name, name const & struct_name, name const & const_name):
+            m_base_struct_name(base_struct_name), m_struct_name(struct_name), m_const_name(const_name) {}
+    };
+
+    /** Field resolution: projection is being used to make a "local" recursive call */
+    struct field_resolution_local_rec {
+        /** The generalized structure name for the argument to the call. */
+        name m_base_struct_name;
+        /** The resolved name for the recursive call (for error reporting). */
+        name m_full_name;
+        /** The declaration for the "local" recursive call. */
+        local_decl m_ldecl;
+
+        field_resolution_local_rec(name const & base_struct_name, name const & full_name, local_decl const & ldecl):
+            m_base_struct_name(base_struct_name), m_full_name(full_name), m_ldecl(ldecl) {}
+    };
+
     struct field_resolution {
-        name m_S_name; // structure name of field expression type
-        name m_base_S_name; // structure name of field
-        name m_fname;
-        optional<local_decl> m_ldecl; // projection is a local constant: recursive call
-
-        field_resolution(name const & full_fname, optional<local_decl> ldecl = {}):
-                m_S_name(full_fname.get_prefix()), m_base_S_name(full_fname.get_prefix()),
-                m_fname(full_fname.get_string()), m_ldecl(ldecl) {}
-        field_resolution(const name & S_name, const name & base_S_name, const name & fname):
-                m_S_name(S_name), m_base_S_name(base_S_name), m_fname(fname) {}
-
-        name get_full_fname() const { return m_base_S_name + m_fname; }
+        /** `ProjFn`: a field projection.
+         * `Const`: a "method" (a.k.a. extended dot notation).
+         * `LocalRec`: a "local" recursive call using field notation. */
+        enum class kind { ProjFn, Const, LocalRec };
+
+        kind m_kind;
+        /** (All kinds) */
+        name m_base_struct_name;
+        /** (ProjFn and Const) */
+        name m_struct_name;
+        /** (ProjFn) `m_field_name`.
+         * (Const) `m_const_name`.
+         * (LocalRec) `m_full_name` (for error reporting). */
+        name m_extra;
+        /** (LocalRec) */
+        local_decl m_ldecl;
+
+        field_resolution(field_resolution_proj_fn const & fr_proj_fn):
+            m_kind(kind::ProjFn),
+            m_base_struct_name(fr_proj_fn.m_base_struct_name),
+            m_struct_name(fr_proj_fn.m_struct_name),
+            m_extra(fr_proj_fn.m_field_name) {}
+        field_resolution(field_resolution_const const & fr_const):
+            m_kind(kind::Const),
+            m_base_struct_name(fr_const.m_base_struct_name),
+            m_struct_name(fr_const.m_struct_name),
+            m_extra(fr_const.m_const_name) {}
+        field_resolution(field_resolution_local_rec const & fr_local_rec):
+            m_kind(kind::LocalRec),
+            m_base_struct_name(fr_local_rec.m_base_struct_name),
+            m_extra(fr_local_rec.m_full_name),
+            m_ldecl(fr_local_rec.m_ldecl) {}
+
+        name get_base_struct_name() const { return m_base_struct_name; }
+        name get_struct_name() const { lean_assert(m_kind == kind::ProjFn || m_kind == kind::Const); return m_struct_name; }
+        name get_field_name() const { lean_assert(m_kind == kind::ProjFn); return m_extra; }
+        name get_const_name() const { lean_assert(m_kind == kind::Const); return m_extra; }
+
+        /** The function name to use when reporting errors associated to this field resolution. */
+        name get_full_name() {
+            switch (m_kind) {
+                case kind::ProjFn: return get_base_struct_name() + get_field_name();
+                case kind::Const: return get_const_name();
+                case kind::LocalRec: return m_extra;
+                default: lean_unreachable();
+            }
+        }
     };
 
-    field_resolution field_to_decl(expr const & e, expr const & s, expr const & s_type);
-    field_resolution find_field_fn(expr const & e, expr const & s, expr const & s_type);
+    field_resolution resolve_field_notation_aux(expr const & e, expr const & s, expr const & s_type);
+    /** \c e is the field notation expression, \c s is the elaborated expression, \c s_type is its type */
+    field_resolution resolve_field_notation(expr const & e, expr const & s, expr const & s_type);
+
     expr visit_field(expr const & e, optional<expr> const & expected_type);
     expr instantiate_mvars(expr const & e, std::function<bool(expr const &)> pred); // NOLINT
     expr visit_structure_instance(expr const & e, optional<expr> expected_type);
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index f421a26f88..3f313848db 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -177,6 +177,31 @@ optional<name> find_field(environment const & env, name const & S_name, name con
     return {};
 }
 
+optional<pair<name, name>> find_method(environment const & env, name const & struct_name, name const & field_name) {
+    if (env.find(struct_name + field_name))
+        return some(mk_pair(struct_name, struct_name + field_name));
+    if (is_structure_like(env, struct_name)) {
+        for (auto const & p : get_parent_structures(env, struct_name)) {
+            if (auto m = find_method(env, p, field_name))
+                return m;
+        }
+    }
+    return {};
+}
+
+optional<pair<name, name>> find_method_alias(environment const & env, name const & struct_name, name const & field_name) {
+    optional<pair<name, name>> res = {};
+    for (auto const & alias : get_expr_aliases(env, struct_name + field_name)) {
+        if (alias.drop_prefix() == field_name) {
+            if (res) {
+                return {};
+            }
+            res = some(mk_pair(alias.get_prefix(), alias));
+        }
+    }
+    return res;
+}
+
 void get_structure_fields_flattened(environment const & env, name const & structure_name, buffer<name> & full_fnames) {
     for (auto const & fname : get_structure_fields(env, structure_name)) {
         full_fnames.push_back(structure_name + fname);
diff --git a/src/frontends/lean/structure_cmd.h b/src/frontends/lean/structure_cmd.h
index 946da1a89b..32d73b5913 100644
--- a/src/frontends/lean/structure_cmd.h
+++ b/src/frontends/lean/structure_cmd.h
@@ -27,6 +27,15 @@ optional<name> find_field(environment const & env, name const & S_name, name con
 optional<expr> mk_base_projections(environment const & env, name const & S_name, name const & base_S_name, expr const & e);
 /** \brief Return an unelaborated expression applying a field projection */
 expr mk_proj_app(environment const & env, name const & S_name, name const & fname, expr const & e, expr const & ref = {});
+/** \brief Searches for `struct_name.field_name` in the environment, and if `struct_name` is a structure,
+ * recursively does the same for its parent structures if the environment contains no such name.
+ * Returns `(S', n)` where S' is the name of the (generalized) structure and n is the name corresponding to \c field_name */
+optional<pair<name, name>> find_method(environment const & env, name const & struct_name, name const & field_name);
+/** \brief If `struct_name.field_name` is uniquely an alias for `struct_name'.field_name` then
+ * returns `(struct_name', struct_name'.field_name)`.
+ *
+ * Should consider generating an error or warning if there is more than one such alias. */
+optional<pair<name, name>> find_method_alias(environment const & env, name const & struct_name, name const & field_name);
 
 /* Default value support */
 optional<name> has_default_value(environment const & env, name const & S_name, name const & fname);
diff --git a/src/library/attribute_manager.h b/src/library/attribute_manager.h
index ec5d59f338..891a0e98e6 100644
--- a/src/library/attribute_manager.h
+++ b/src/library/attribute_manager.h
@@ -260,7 +260,7 @@ struct key_value_data : public attr_data {
 /** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */
 typedef typed_attribute<indices_attribute_data> indices_attribute;
 
-/** \brief Attribute that represents a list of indices. input and output are 1-indexed for convenience. */
+/** \brief Attribute that represents a single key/value pair. */
 typedef typed_attribute<key_value_data> key_value_attribute;
 
 class user_attribute_ext {
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 12ef730c4d..b7188a0fb8 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -67,6 +67,7 @@ name const * g_forall_congr = nullptr;
 name const * g_forall_congr_eq = nullptr;
 name const * g_forall_not_of_not_exists = nullptr;
 name const * g_format = nullptr;
+name const * g_function = nullptr;
 name const * g_funext = nullptr;
 name const * g_has_add = nullptr;
 name const * g_has_add_add = nullptr;
@@ -349,6 +350,7 @@ void initialize_constants() {
     g_forall_congr_eq = new name{"forall_congr_eq"};
     g_forall_not_of_not_exists = new name{"forall_not_of_not_exists"};
     g_format = new name{"format"};
+    g_function = new name{"function"};
     g_funext = new name{"funext"};
     g_has_add = new name{"has_add"};
     g_has_add_add = new name{"has_add", "add"};
@@ -632,6 +634,7 @@ void finalize_constants() {
     delete g_forall_congr_eq;
     delete g_forall_not_of_not_exists;
     delete g_format;
+    delete g_function;
     delete g_funext;
     delete g_has_add;
     delete g_has_add_add;
@@ -914,6 +917,7 @@ name const & get_forall_congr_name() { return *g_forall_congr; }
 name const & get_forall_congr_eq_name() { return *g_forall_congr_eq; }
 name const & get_forall_not_of_not_exists_name() { return *g_forall_not_of_not_exists; }
 name const & get_format_name() { return *g_format; }
+name const & get_function_name() { return *g_function; }
 name const & get_funext_name() { return *g_funext; }
 name const & get_has_add_name() { return *g_has_add; }
 name const & get_has_add_add_name() { return *g_has_add_add; }
diff --git a/src/library/constants.h b/src/library/constants.h
index b5a0861f0e..da2921cad3 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -69,6 +69,7 @@ name const & get_forall_congr_name();
 name const & get_forall_congr_eq_name();
 name const & get_forall_not_of_not_exists_name();
 name const & get_format_name();
+name const & get_function_name();
 name const & get_funext_name();
 name const & get_has_add_name();
 name const & get_has_add_add_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 9605ba8f3d..ad69ff3ffe 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -62,6 +62,7 @@ forall_congr
 forall_congr_eq
 forall_not_of_not_exists
 format
+function
 funext
 has_add
 has_add.add
diff --git a/tests/lean/assertion1.lean.expected.out b/tests/lean/assertion1.lean.expected.out
index 2f31b707b2..4e6c8e58c2 100644
--- a/tests/lean/assertion1.lean.expected.out
+++ b/tests/lean/assertion1.lean.expected.out
@@ -1 +1,19 @@
-assertion1.lean:37:21: error: invalid field notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...)
+assertion1.lean:37:21: error: type mismatch at application
+  MonoidalCategory.tensorObjects C
+term
+  C
+has type
+  MonoidalCategory : Type (max (u+1) (v+1))
+but is expected to have type
+  ?m_1.carrier.Obj : Type ?
+Additional information:
+assertion1.lean:37:21: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
+  type mismatch at application
+    MonoidalCategory.tensorObjects C
+  term
+    C
+  has type
+    MonoidalCategory : Type (max (u+1) (v+1))
+  but is expected to have type
+    ?m_1.carrier.Obj : Type ?
+assertion1.lean:37:21: context: invalid field notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...)
diff --git a/tests/lean/field_resolution.lean b/tests/lean/field_resolution.lean
new file mode 100644
index 0000000000..ea5bcd42cc
--- /dev/null
+++ b/tests/lean/field_resolution.lean
@@ -0,0 +1,136 @@
+section structures
+
+structure foo :=
+(a : ℕ)
+
+structure bar extends foo :=
+(b : ℕ)
+
+def foo.s : foo := {a := 37}
+def bar.s : bar := {a := 17, b := 22}
+
+-- (error) prefer "unknown identifier"
+#check foo.c
+
+-- true fields
+#eval foo.s.a
+#eval bar.s.a
+#eval bar.s.b
+
+-- anonymous field notation
+#eval foo.s.1
+#eval bar.s.1.1
+#eval bar.s.2
+
+def foo.inc_a (s : foo) : ℕ := s.a + 1
+def bar.inc_b (s : bar) : ℕ := s.b + 1
+
+-- extended dot notation (method resolution)
+#eval foo.s.inc_a
+#eval bar.s.inc_a
+#eval bar.s.inc_b
+
+def foo.add_a (n : ℕ) (s : foo) : ℕ := s.a + n
+
+example : foo.s.add_a 1 = foo.s.inc_a := rfl
+example : bar.s.add_a 1 = bar.s.inc_a := rfl
+
+-- (error) insufficient arguments is error (yet could be lambda like in Lean 4)
+#check foo.s.add_a
+--example : foo.s.add_a = λ n, foo.s.add_a n := rfl
+#check bar.s.add_a
+--example : bar.s.add_a = λ n, bar.s.add_a n := rfl
+
+def foo.add_b_of_eq (n : ℕ) {m : ℕ} (h : n = m) (s : foo) : ℕ := s.a + m
+
+-- (error) insufficient arguments (trickier example for synthesizing lambda)
+#check foo.s.add_b_of_eq
+
+def foo.blah (n : ℕ) : ℕ := n
+
+-- (error) invalid field notation, no explicit argument of type (foo ...)
+#check foo.s.blah 37
+#check bar.s.blah 37
+
+structure implicit_test := (f : ∀ {m : ℕ}, m = 0)
+
+variables (s : implicit_test)
+#check (s.f : 37 = 0) -- before #757 would have been (s.f : ∀ {m : ℕ}, m = 0)
+#check (λ _, s.f : ∀ {m : ℕ}, m = 0)
+
+end structures
+
+section local_constants
+
+-- Without arguments
+def list.double {α : Type*} : list α → list α
+| [] := []
+| (x :: xs) := x :: x :: xs.double
+
+-- With arguments (and list argument after first, fixed in #757)
+def list.map' {α β : Type*} : (α → β) → list α → list β
+| _ [] := []
+| f (x :: xs) := f x :: xs.map' f
+
+def list.map'' {α β : Type*} : list α → (α → β) → list β
+| [] _ := []
+| (x :: xs) f := f x :: xs.map' f
+
+end local_constants
+
+section classes
+
+class baz (α : Type*) :=
+(a : α)
+(b : ℕ → α)
+
+-- projection for class instance
+example (α : Type*) (I : baz α) : I.a = I.a := rfl
+-- projection for class instance with arguments
+example (α : Type*) (I : baz α) : I.b 37 = I.b 37 := rfl
+-- plain fully qualified name
+example (α : Type*) [baz α] : (baz.b 37 : α) = baz.b 37 := rfl
+
+end classes
+
+section functions
+
+lemma function.mt {p q : Prop} (h : p → q) : ¬ q → ¬ p := mt h
+
+example {p q : Prop} (hnp : ¬ p) (h : q → p) : ¬ q := h.mt hnp
+
+def function.apply {α β : Type*} (x : α) (f : α → β) : β := f x
+
+example : (+ 3).apply 1 = 4 := rfl
+-- (error) insufficient number of arguments is error (yet could be a lambda like in Lean 4)
+#check λ (x : ℕ), (+ x).apply
+--example : (λ (x : ℕ), (+ x).apply) = (λ x y, y + x) := rfl
+--example : (λ (x : ℕ), (+ x).apply) = (λ (y : ℕ), (+ y).apply) := rfl
+
+end functions
+
+section aliases
+
+def Set (α : Type) := α → Prop
+def Set.union {α : Type} (s₁ s₂ : Set α) : Set α := λ a, s₁ a ∨ s₂ a
+def FinSet (n : ℕ) := fin n → Prop
+
+export Set (renaming union → FinSet.union)
+
+example (x y : FinSet 10) : FinSet 10 :=
+  x.union y -- Works
+
+end aliases
+
+section first_arg
+
+instance (p q : Prop) : has_coe_to_fun (p ↔ q) (λ _, p → q) := ⟨λ h, h.mp⟩
+
+structure my_prop (p : Prop) : Prop := (h : p)
+
+def my_prop.iff {p : Prop} : my_prop p ↔ p := ⟨my_prop.h, λ h, ⟨h⟩⟩
+
+-- Use the first explicit argument
+example (p : Prop) (h : my_prop p) : p := h.iff
+
+end first_arg
diff --git a/tests/lean/field_resolution.lean.expected.out b/tests/lean/field_resolution.lean.expected.out
new file mode 100644
index 0000000000..534e806ab6
--- /dev/null
+++ b/tests/lean/field_resolution.lean.expected.out
@@ -0,0 +1,40 @@
+field_resolution.lean:13:7: error: unknown identifier 'foo.c'
+37
+17
+22
+37
+17
+22
+38
+18
+23
+field_resolution.lean:39:12: error: invalid field notation, insufficient number of arguments for 'foo.add_a'
+foo.add_a ⁇ foo.s : ℕ
+field_resolution.lean:41:12: error: invalid field notation, insufficient number of arguments for 'foo.add_a'
+foo.add_a ⁇ bar.s.to_foo : ℕ
+field_resolution.lean:47:12: error: invalid field notation, insufficient number of arguments for 'foo.add_b_of_eq'
+foo.add_b_of_eq ⁇ _ foo.s : ℕ
+field_resolution.lean:52:12: error: type mismatch at application
+  foo.blah foo.s
+term
+  foo.s
+has type
+  foo
+but is expected to have type
+  ℕ
+Additional information:
+field_resolution.lean:52:12: context: invalid field notation, function 'foo.blah' does not have explicit argument with type (foo ...)
+field_resolution.lean:53:12: error: type mismatch at application
+  foo.blah bar.s.to_foo
+term
+  bar.s.to_foo
+has type
+  foo
+but is expected to have type
+  ℕ
+Additional information:
+field_resolution.lean:53:12: context: invalid field notation, function 'foo.blah' does not have explicit argument with type (foo ...)
+s.f : 37 = 0
+λ (_x : ℕ), s.f : ∀ (_x : ℕ), _x = 0
+field_resolution.lean:106:23: error: invalid field notation, insufficient number of arguments for 'function.apply'
+λ (x : ℕ), function.apply ⁇ (λ (_x : ℕ), _x + x) : ℕ → ℕ
diff --git a/tests/lean/interactive/field_info.lean.expected.out b/tests/lean/interactive/field_info.lean.expected.out
index a41f29c66f..8c724a6796 100644
--- a/tests/lean/interactive/field_info.lean.expected.out
+++ b/tests/lean/interactive/field_info.lean.expected.out
@@ -1,7 +1,7 @@
 {"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n  n\nwhich has type\n  ℕ"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n  n\nwhich has type\n  ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n  n\nwhich has type\n  ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"},{"caption":"","file_name":"field_info.lean","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n  n\nwhich has type\n  ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"},{"caption":"","file_name":"field_info.lean","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"field_info.lean","pos_col":0,"pos_line":12,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":1,"severity":"error","text":"invalid field notation, 'to_string' is not a valid \"field\" because environment does not contain 'nat.to_string'\n  n\nwhich has type\n  ℕ"},{"caption":"","file_name":"field_info.lean","pos_col":4,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\nn : ℕ\n⊢ Sort ?"},{"caption":"","file_name":"field_info.lean","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"field_info.lean","pos_col":18,"pos_line":12,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"state":"n : ℕ\n⊢ ⁇"},"response":"ok","seq_num":2}
 {"record":{"full-id":"list.all","source":,"state":"l : list ℕ\n⊢ (ℕ → bool) → bool","type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":4}