mathlib3

A `ring_exp` tactic for dealing with exponents in rings

#1715

Merged