mathlib3 documentation

core / init.meta.async_tactic

meta def tactic.run_async {α : Type} (tac : tactic α) :

Proves the first goal asynchronously as a separate lemma.