mathlib documentation

core / init.meta.relation_tactics

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

Try to apply subst exhaustively