fix: make sure anonymous dot notation works with type synonyms

When resolving anonymous dot notation (`.ident x y z`), it would reduce the expected type to whnf. Now, it unfolds definitions step-by-step, even if the type synonym is for a pi type like so
```lean
def Foo : Prop := ∀ a : Nat, a = a
protected theorem Foo.intro : Foo := sorry
example : Foo := .intro
```

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

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