Should `nat.pow_left_inj` exist?

Stream: Lean for the curious mathematician 2020

[Eric Wieser]

Something that came up repeatedly in our breakout is that pow_left_inj creates some ugly conversions between two different types of power operator. Would it make sense to add this lemma to mathlib to avoid that ugliness?

lemma nat.pow_left_inj {x y : ℕ} {n : ℕ} (Hnpos : 0 < n)
  (Hxyn : x ^ n = y ^ n) : x = y :=
  pow_left_inj (nat.zero_le _) (nat.zero_le _) Hnpos (by simp [Hxyn])

[Anne Baanen]

I agree it's worth it to add this, especially since the lemma fills in the nonnegativity assumptions. The cleaner solution is to remove nat.has_pow entirely, but there are implementation issues with this.

[Patrick Massot]

I think getting rid of this stupid nat.has_pow should have really high priority.

[Patrick Massot]

People who want it for programming should use a different notation (or no notation at all).

[Patrick Massot]

I'm very upset that participants in my breakout room lost so much time because of this issue.

[Anatole Dedecker]

I think I had a similar problem a few months ago when I tried to prove irrationality of sqrt2, and the fix you told me was something like "don't use ^2" :laughing:

[Patrick Massot]

Indeed Anatole, it's the very same issue. We simply need to fix it once and for all.