diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 14c0ae70d636..cbbee7da1212 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1354,9 +1354,17 @@ private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) :
   tryPostponeIfNoneOrMVar expectedType?
   let some expectedType := expectedType?
     | throwError "invalid dotted identifier notation, expected type must be known"
-  forallTelescopeReducing expectedType fun _ resultType => do
+  withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
+  /-- A weak version of forallTelescopeReducing that only uses whnfCore. -/
+  withForallBody {α} (type : Expr) (k : Expr → TermElabM α) : TermElabM α :=
+    forallTelescope type fun _ body => do
+      let body ← whnfCore body
+      if body.isForall then
+        withForallBody body k
+      else
+        k body
   go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Name := do
     let resultType ← instantiateMVars resultType
     let resultTypeFn := resultType.cleanupAnnotations.getAppFn
@@ -1372,7 +1380,8 @@ where
       | ex@(.error ..) =>
         match (← unfoldDefinition? resultType) with
         | some resultType =>
-          go (← whnfCore resultType) expectedType (previousExceptions.push ex)
+          withForallBody resultType fun resultType => do
+            go resultType expectedType (previousExceptions.push ex)
         | none =>
           previousExceptions.forM fun ex => logException ex
           throw ex
diff --git a/tests/lean/run/4761.lean b/tests/lean/run/4761.lean
new file mode 100644
index 000000000000..56feeba7b039
--- /dev/null
+++ b/tests/lean/run/4761.lean
@@ -0,0 +1,8 @@
+/-!
+# Make sure "anonymous dot notation" works with type synonyms.
+-/
+
+def Foo : Prop := ∀ a : Nat, a = a
+
+protected theorem Foo.intro : Foo := sorry
+example : Foo := .intro