Data.PNat.Factors !4#1830

Stream: mathlib4

[Ruben Van de Velde]

This has an odd error where apparently lean can't find the Pow ℕ+ ℕ instance. Would be great if someone could take a look

[Lukas Miaskiwskyi]

I definitely have seen Pow errors like this before, and the common solution seems to be replacing a^b with Pow.pow a b, but that is not ideal indeed. An example with a useful porting note is in Data.PNat.Basic:

-- Porting note:
-- mathlib3 statement was
-- `((m ^ n : ℕ+) : ℕ) = (m : ℕ) ^ n`
-- where the left `^ : ℕ+ → ℕ → ℕ+` was `monoid.has_pow`.
-- Atm writing `m ^ n` means automatically `(↑m) ^ n`.
@[simp, norm_cast]
theorem pow_coe (m : ℕ+) (n : ℕ) : ((Pow.pow m n : ℕ+) : ℕ) = (m : ℕ) ^ n :=
  rfl
#align pnat.pow_coe PNat.pow_coe

How do we get ^ to behave more naturally?

[Eric Wieser]

Is docs4#instHPow a thing?

[Eric Wieser]

Oh, it's already a default instance