mathlib

fa0a4d63 - fix(tactic/ring): perform definitional rather than syntactic matches on `^`