From 520cd3f0d64732d8cd8d4acea69cdd7624ea5a2d Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 27 Mar 2024 17:59:09 -0700
Subject: [PATCH] fix: make generalized field notation for abbreviation types
 handle optional parameters (#3746)

Closes #3745
---
 src/Lean/Elab/App.lean   |  2 +-
 tests/lean/run/3745.lean | 31 +++++++++++++++++++++++++++++++
 2 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/3745.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 9528eea8d0..c90c79ea84 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/tests/lean/run/3745.lean b/tests/lean/run/3745.lean
new file mode 100644
index 0000000000..eff827f09c
--- /dev/null
+++ b/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