mathlib

0c70cf30 - feat(tactic/unify_equations): add unify_equations tactic (#4515)

feat(tactic/unify_equations): add unify_equations tactic (#4515) `unify_equations` is a first-order unification tactic for propositional equalities. It implements the algorithm that `cases` uses to simplify indices of inductive types, with one extension: `unify_equations` can derive a contradiction from 'cyclic' equations like `n = n + 1`. `unify_equations` is unlikely to be particularly useful on its own, but I'll use it as part of my new `induction` tactic.