diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 6e0a67bd7b..b8f1369bd5 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2426,8 +2426,11 @@ expr elaborator::visit_field(expr const & e, optional<expr> const & expected_typ
     expr proj  = copy_tag(e, mk_constant(full_fname));
     expr new_e = copy_tag(e, mk_app(proj, copy_tag(e, mk_as_is(s))));
     expr r = visit(new_e, expected_type);
-    if (auto pos = get_field_notation_field_pos(e))
-        save_identifier_info(app_fn(r), pos);
+    if (is_app(r)) {
+        /* r may be a sorry macro due to error recovery*/
+        if (auto pos = get_field_notation_field_pos(e))
+            save_identifier_info(app_fn(r), pos);
+    }
     return r;
 }
 
diff --git a/tests/lean/run/assertion1.lean b/tests/lean/run/assertion1.lean
new file mode 100644
index 0000000000..b14428f236
--- /dev/null
+++ b/tests/lean/run/assertion1.lean
@@ -0,0 +1,38 @@
+universe variables u v
+
+structure Category :=
+  (Obj : Type u)
+  (Hom : Obj → Obj → Type v)
+
+universe variables u1 v1 u2 v2
+
+structure Functor (C : Category.{ u1 v1 }) (D : Category.{ u2 v2 }) :=
+  (onObjects   : C^.Obj → D^.Obj)
+
+@[reducible] definition ProductCategory (C : Category) (D : Category) :
+  Category :=
+  {
+    Obj      := C^.Obj × D^.Obj,
+    Hom      := (λ X Y : C^.Obj × D^.Obj, C^.Hom (X^.fst) (Y^.fst) × D^.Hom (X^.snd) (Y^.snd))
+  }
+
+namespace ProductCategory
+  notation C `×` D := ProductCategory C D
+end ProductCategory
+
+@[reducible] definition TensorProduct ( C: Category ) := Functor ( C × C ) C
+
+structure MonoidalCategory
+  extends carrier : Category :=
+  (tensor : TensorProduct carrier)
+
+instance MonoidalCategory_coercion : has_coe MonoidalCategory Category :=
+  ⟨MonoidalCategory.to_Category⟩
+
+-- Convenience methods which take two arguments, rather than a pair. (This seems to often help the elaborator avoid getting stuck on `prod.mk`.)
+@[reducible] definition MonoidalCategory.tensorObjects { C : MonoidalCategory } ( X Y : C^.Obj ) : C^.Obj := C^.tensor^.onObjects (X, Y)
+
+definition tensor_on_left { C: MonoidalCategory.{u v} } ( Z: C^.Obj ) : Functor.{u v u v} C C :=
+{
+  onObjects := λ X, C^.tensorObjects Z X
+}