Peculiar behaviour of `refine` tactic

Stream: lean4

[Anand Rao Tadipatri]

In the MWE below, the first proof succeeds as I would expect, but the second one with refine fails, even there is no discernable difference between the tactic states of the two examples. This issue holds even with the refine' tactic. Is this expected behaviour for refine?

import Mathlib.Tactic

set_option autoImplicit false

example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by
  constructor
  assumption

example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by
  refine ⟨?_, ?_⟩
  swap
  assumption -- fails

[Kyle Miller]

@Anand Rao Tadipatri I created an issue: lean4#2361

[Anand Rao Tadipatri]

Thank you!