doing casts with `simp`

Stream: general

[Kevin Buzzard]

import set_theory.cardinal

example (m n : ℕ) : (↑m : cardinal) = ↑n → m = n := by simp -- works fine

example (m n : ℕ) (H : (↑m : cardinal) = ↑n) : m = n := by simp [H] -- fails

Is there a way of getting the second example to work which doesn't involve (a) reverting H or (b) looking up the name of the lemma which simp is using to do the cast [i guess it's going to be cardinal.nat_cast_inj, maybe I'm supposed to know that]. Neither (a) nor (b) look "idiomatic" to me (is that the right word?)

[Rob Lewis]

simpa using H?

[Kenny Lau]

why are you doing cardinals? @Kevin Buzzard

[Kevin Buzzard]

Richard Thomas asked a question about the number 3

[Kevin Buzzard]

but then complained when I assumed it was finite