Tactic to "name" a goal and use it afterwards

Stream: Is there code for X?

[Antoine Chambert-Loir]

Sometimes, applying stuff produces many redundant goals. Is there a tactic that names the present goal so that it can be reused in all further goals (which are below).
One thing that worked in one case is doing

suffices : _,

early enough, and then

exact this,

but I find it a bit awkward.

[Johan Commelin]

You can

have very_useful := _,
may,
great,
tactics,
apply powerful_lemma 37 _ _ _ very_useful _ _ _,
-- now there might be 7 goals, and you can use `very_useful` in all of them

[Johan Commelin]

It still feels a bit hacky, and I think we should have better tactic support for this.

[Johan Commelin]

Note that Lean 4 has more bells and whistles in this direction, namely named metavariables

[Mario Carneiro]

Yeah I have used suffices, for this before

[Antoine Chambert-Loir]

One case where this is useful is when simply "copy-pasting" the goal doesn't work because of coercions arrow, or arguments which are replaced by underscores…