Feature Request: `ext?`

I am requesting a tactic ext? as the ? analogue of ext. Like the other ? tactics (simp?, exact?, apply?), it would output a clickable text in the infoview that would replace the call to ext?.

The result of the conversion would look like refine [ext_lemma] fun i ↦ ?_. In the case of two or more @[ext] lemmas being applied, the result should also show this.

Zulip discussion: #Is there code for X? > ext?

Testcase:

import Mathlib

lemma test {X Y Z : Type*} (f g : X → Y → Z) : f = g := by
  ext x y
  -- ⊢ f x y = g x y
  sorry

Here ext? x y would be expected to produce the clickable text replacing itself with refine funext fun x ↦ funext fun y ↦ ?_.

Start from the existing ext tactic and the analogous simp?, exact?, and apply? tactics, then use the supplied testcase to inspect the expected infoview output. Done means ext? produces clickable replacement text for one or multiple extension lemmas, including the shown nested funext form.