apply bug: `sorry` is falsely claimed as "no goals"

Stream: lean4

[Michael Rothgang]

I believe I found a bug in apply. In the following code, refine works, but apply claims a sorry is not necessary. The following bug reproduced on the playground (i.e., latest mathlib), but also on Lean 4.12.

import Mathlib.MeasureTheory.Integral.Lebesgue
import Mathlib.Order.CompletePartialOrder

open scoped NNReal ENNReal
variable {X : Type*} [MeasureTheory.MeasureSpace X]

-- the actual definition is an expression involving y (and extra parameters).
noncomputable def cutoff (_y : X) : ℝ≥0 := ⟨37, by positivity⟩

theorem lintegral_monoOn {α : Type*} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
    {s : Set α} ⦃f g : α → ℝ≥0∞⦄ (hfg : ∀ x : s, f x ≤ g x) :
    ∫⁻ a in s, f a ∂μ ≤ ∫⁻ a in s, g a ∂μ := by sorry

lemma errors {s : Set X} {x y : X} : ∫⁻ y in s, 35 ≤ ∫⁻ y in s, (cutoff y) := by
      -- This is fine: `refine` accepts this code.
      -- bug: replacing "refine" by "apply" yields an error "no goals to be solved" on the sorry
      -- (which is bogus: removing the sorry leads to the expected goal state)
      refine lintegral_monoOn fun ⟨y', hy'⟩ ↦ ?_
      sorry

I presume this is a core bug. If not, please feel free to move to the mathlib4 stream!

[Michael Rothgang]

I minimized the imports; help diagnosing or minimizing this (e.g., making mathlib-free) would be very welcome!

[Joachim Breitner]

I don’t think apply supports the ?_ syntax to create new goals, and if I just write

apply (lintegral_monoOn fun ⟨y', hy'⟩ ↦ ?_)

then I get an error on ?_ saying

don't know how to synthesize placeholder

[Mauricio Collares]

You can use it in some situations: rg apply | grep "?_" | wc -l on Mathlib prints 518, and there aren't too many grep false positives.

[Mauricio Collares]

For example https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Function/Jacobian.lean#L583

[Mauricio Collares]

(@Gabriel Dahia told me this less than a month ago and I was very surprised)

[Mauricio Collares]

What's super fun about @Michael Rothgang's example is that you get different behavior if you remove the pattern match and write apply lintegral_monoOn fun arg => ?_ instead

[Joachim Breitner]

Hmm, ok, I take that back then. I thought there is a difference between how refine and apply treat ?_?

[Kyle Miller]

I'm guessing this is a bug in apply due to how the match fun is being elaborated (matches can be postponed, and it seems that it's being postponed until after apply figures out the new goals). It would be great if someone could find a mathlib-free example!