tactic to name a ✝ variable

Stream: mathlib4

[Heather Macbeth]

Can someone please remind me of the name of the tactic which names the first ✝ variable around? I have no idea how to search for this in documentation, unfortunately.

[Mario Carneiro]

next a =>, or rename_i a

[Jannis Limperg]

(The daggered names are called "inaccessible".)