mathlib3

feat(tactic/equiv_rw): rewriting along equivalences

#2246

Merged