Feature Request: `ext?`

[kckennylau]

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 ↦ ?_.