ring_exp needs ring

Stream: general

[Patrick Massot]

@Anne Baanen, I find the following proof disappointing. I didn't expect the second line.

example (n : ℕ) : 2 ^ (n + 1 + 1)  = 2 * 2 ^ (n + 1) :=
begin
  ring_exp,
  ring,
end

[Jalex Stark]

There are also examples where ring requires another application of ring, right?

[Kevin Buzzard]

I've had to apply ring twice in some situations but this is probably due to some metavariable bug

[Reid Barton]

I know at least some instances of this were fixed: https://github.com/rwbarton/lean-homotopy-theory/commit/6f1ae4e1b22897cbd0d240926601b4005a9c9994#diff-e3c5121260ab4a6628611e784c1695edL90

[Anne Baanen]

Thanks for the report! It turns out norm_num didn't get called in this case, which is fixed in this PR.