mathlib3

fix(tactic/elide): was untested and buggy. Fixed a few issues

#1638

Merged