using (or making explicit) hidden assumptions?

Stream: lean4

[Thomas Murrills]

Can you refer to an automatically-generated hidden assumption (like h✝) explicitly in a tactic somehow (e.g., so that it does what you'd naively expect rw [h✝] to do)? If not, is there some standard way to make them explicit once they already exist in the context?

[Thomas Murrills]

(In particular, I'm looking to refer to some of the assumptions split introduced.)

[Arien Malec]

rename_i renames the last automatically introduced hygenic names.

[Mario Carneiro]

In a tactic, you should use FVarId to refer to hypotheses instead of user names where possible