tactic to convert current goals into a closed lemma

Stream: general

[acertain]

is there a tactic somewhere to convert the current goal context into a lemma/term (replace metas with exists, revert hypotheses, conjoin goals)?

[Scott Morrison]

extract_goal (doesn't do everything in your parentheses, however!)