mathlib documentation

core / init.meta.constructor_tactic

meta def tactic.left  :

meta def tactic.existsi (e : expr) :