fix: make generalized field notation for abbreviation types handle optional parameters

src/Lean/Elab/App.lean

@@ -1149,7 +1149,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
 private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   if baseName == `Function then
     return (← whnfR type).isForall
-  else if type.consumeMData.isAppOf baseName then
+  else if type.cleanupAnnotations.isAppOf baseName then
     return true
   else
     return (← whnfR type).isAppOf baseName

tests/lean/run/3745.lean

@@ -0,0 +1,31 @@
+/-!
+# Issue 3745
+
+Field notation for abbreviations would fail if the argument for field notation was an optional parameter.
+-/
+
+structure A
+
+abbrev B := A
+
+def A.x (_ : A) := 1
+def B.x (_ : B) := 2
+
+def A.y (_ : A) := 1
+def B.y (_ : B := {}) := 2
+
+/-!
+These were OK before the fix.
+-/
+/-- info: 1 -/
+#guard_msgs in #eval (show A from {}).x
+/-- info: 2 -/
+#guard_msgs in #eval (show B from {}).x
+
+/-!
+The second of these failed before the fix.
+-/
+/-- info: 1 -/
+#guard_msgs in #eval (show A from {}).y
+/-- info: 2 -/
+#guard_msgs in #eval (show B from {}).y