mathlib documentation

core.init.meta.async_tactic

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

Proves the first goal asynchronously as a separate lemma.