How to save the current goal / subgoal as an `assert` lemma

Question

During a proof, I come to a situation where the current goal/subgoal turned out to be useful in a later stage of the same theorem.

Is there a tactic to "save" the current goal as a lemma as if the current goal is asserted?

Of course, I can copy&paste to assert the goal explicitly, or write a separate Lemma before the current theorem. But I am just curious if shortcuts exist.

Thanks.

Answer 1

To my knowledge, there is no such feature in Coq, and neither CoqIDE nor ProofGeneral seems to provide one.