mathlib3 documentation

core / init.meta.relation_tactics

meta def tactic.reflexivity (md : tactic.transparency := tactic.transparency.semireducible) :

meta def tactic.symmetry (md : tactic.transparency := tactic.transparency.semireducible) :

meta def tactic.transitivity (md : tactic.transparency := tactic.transparency.semireducible) :

meta def tactic.relation_lhs_rhs (e : expr) :

tactic (name × expr × expr)

meta def tactic.target_lhs_rhs :

tactic (name × expr × expr)

If the main target has the form r lhs rhs, then return (r,lhs,rhs).

meta def tactic.subst_vars :

Try to apply subst exhaustively