Blanks in apply

Stream: lean4

[Dan Velleman]

The following two examples work:

example (P Q : Nat → Prop) (h1 : P 0) (h2 : Q 0) : ∃ (x : Nat), P x ∧ Q x := by
  apply Exists.intro 0
  apply And.intro _ h2
  exact h1

example (P Q : Nat → Prop) (h1 : P 0) (h2 : Q 0) : ∃ (x : Nat), P x ∧ Q x := by
  refine Exists.intro 0 (And.intro ?_ h2)
  exact h1

But this one doesn't:

example (P Q : Nat → Prop) (h1 : P 0) (h2 : Q 0) : ∃ (x : Nat), P x ∧ Q x := by
  apply Exists.intro 0 (And.intro _ h2)
  exact h1

Should it? The first example shows that apply can deal with a blank in the middle of an expression. Why can't it deal with the blank in the last example, even though refine can?

[Leonardo de Moura]

The tactics refine <term> and exact <term> elaborate <term> using the expected type ∃ (x : Nat), P x ∧ Q x. apply <term> does not.