`apply` reports "no goals" even when there are still holes in the term

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

apply sometimes falsely reports "no goals", even if the term contains meta-variables. This in particular seems to occur inside of lambda expressions and inside match expressions.

Context

I'm working on a no axioms implementation of real numbers and apply h.elim fun b hb => ?_ is a common paradigm to use instead of obtain ⟨b, hb⟩ := h.

Steps to Reproduce

example (h : ∃ a, 1 < a ∧ a < 4) : True := by
  apply h.elim fun b ⟨hb, hb'⟩ => ?_

Expected behavior: The hole marked by ?_ should become a new goal.

Actual behavior: apply reports "no goals" and you get a "don't know how to synthesize placeholder" error message.

Versions

Lean 4.23.0-nightly-2025-07-09

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the self-contained example against the stated Lean nightly version and confirm whether the placeholder remains unsolved while apply reports no goals. Trace the apply handling for terms inside lambda and match expressions; done means the placeholder becomes a new goal and the reproducer no longer reports the synthesis error.