fixes against the latest mathlib

Stream: general

[Kenny Lau]

now there is a global ^ called pow, and now the type of n will not be inferred from f^n (you need to manually state that n is of type nat). In that case, pow unfolds to monoid.pow, which can be unfolded as before the latest version.

[Kevin Buzzard]

Are you talking about the nightly from the 6th?

[Kenny Lau]

right

[Chris Hughes]

So no more nat.pow?

[Kenny Lau]

I have not tested, but I believe Lean figures out whether you mean monoid.pow or nat.pow

[Kenny Lau]

depending on the first argument

[Chris Hughes]

Getting rid of local infix ^ := monoid.pow seems to help, so it uses has_pow.pow which is definitionally equal, but has rw lemmas.