mathlib documentation

core.init.meta.constructor_tactic

meta def tactic.left  :

meta def tactic.existsi  :