Simp USize.toNat of a numeric literal

Stream: new members

[Julien Michel]

As I think it's more natural to reason about Nat's, I expected Lean to simplify USize.toNat 17 to 17 % USize.size.
So I decided to add a simp lemma, but it doesn't work :

@[simp] theorem th (x : Nat) : USize.toNat (OfNat.ofNat x) = x % USize.size := rfl
example : USize.toNat 17 = 17 % USize.size := by simp -- fails
example : USize.toNat (OfNat.ofNat 17) = 17 % USize.size := by simp -- fails

rw [th] works, simp [th _] works, but simp doesn't work, nor does simp [th]
Why is that?

[Eric Wieser]

Two things:

• You need an OfNat on both sides
• You need to use no_index on the LHS, look at other ofNat lemmas in mathlib for inspiration. There is a note about this, but our tools for linking to said note I think are still out of action.