exact? suggestion contains metavariable

[dwrensha]

When exact? succeeds, I expect it to give me something that closes the current goal.

However, in the following example, the exact? tactic suggests Try this: refine fun a a_1 => ?_.

def Subgroup' (G : Type) [Mul G] : Type := sorry

instance (G : Type) [Mul G] : Membership G (Subgroup' G) := sorry

def iSup' {G : Type} [Mul G] {ι : Type} (S : ι → Subgroup' G) : Subgroup' G := sorry

theorem mem_iSup_of_mem' {G : Type} [Mul G] {ι : Type} {S : ι → Subgroup' G} (i : ι) :
  ∀ {x : G}, x ∈ S i → x ∈ iSup' S := sorry

theorem foo {G : Type}
    [Mul G] {ι : Type} (S : ι → Subgroup' G)
    {C : (x : G) → x ∈ iSup' S → Prop}
    (hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x (mem_iSup_of_mem' i hx))
    (x y : G) :
    (fun x ↦ ∃ (h : x ∈ iSup' S), C x h) x →
      (fun x ↦ ∃ (h : x ∈ iSup' S ), C x h) y →
        (fun x ↦ ∃ (h : x ∈ iSup' S), C x h) (x * y) := by
  exact?
-- Try this: refine fun a a_1 => ?_
-- (kernel) declaration has metavariables 'foo'

This occurs on current nightly and on leanprover/lean4:v4.15.0-rc1

[dwrensha]

The above example was minimized from this line in the proof of Subgroup.iSup_induction' in mathlib.