Tactics
intro H.Implication or universal introduction
intros.Introduce all available binders with automatic names
exact H.Close with a fact
apply H.Backward reasoning
specialize H a as Ha.Universal elimination
obtain x Hx from H.Existential elimination
put theorem_name.Add a previous theorem as an assumption
refl.Equality reflexivity
split.Conjunction or equivalence
cases H.Eliminate a hypothesis
left. / right.Disjunction introduction
use x.Existential witness
resolution.First-order resolution
separation ….Separation schema
replacement ….Replacement schema
