mathlib3

f096a74a - fix(tactic/ring_exp): `ring_exp` now recognizes that `2^(n+1+1) = 2 * 2^(n+1)` (#2929)

fix(tactic/ring_exp): `ring_exp` now recognizes that `2^(n+1+1) = 2 * 2^(n+1)` (#2929) [Zulip thread with bug report](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ring_exp.20needs.20ring). The problem was a missing lemma so that `norm_num` could fire on `x^y` if `x` and `y` are coefficients.