natCast_inj

Stream: lean4

[Cody Roux]

I'm trying to prove ↑n = ↑m → n = m where n, m : ℕ and the equality is at the reals. I assume there's either a lemma for this somewhere or some nuclear tactic. Is that correct?

[Cody Roux]

BTW, apply? really does not seem to help, unfortunately.

[Terence Tao]

hint leads to docs#Nat.cast_inj which works just fine.

[Eric Wieser]

Indeed, exact? does not work here:

import Mathlib

example {m n : ℕ} (h : (↑n : ℝ) = ↑m) : n = m := by exact?

[Eric Wieser]

Nat.cast_injective is the exact statement of your question:

example {m n : ℕ} : (↑n : ℝ) = ↑m → n = m := (Nat.cast_injective ·)

[Cody Roux]

Thanks!

[Kevin Buzzard]

In 2018 you had to learn all of these function names to move between nat, int, rat, real and complex (there was even a cheat sheet!). But nowadays we have the norm_cast and push_cast tactics (and friends such as assumption_mod_cast) which do all the dirty work for you automatically.

[Cody Roux]

Wow norm_cast is a godsend!

[Kevin Buzzard]

We spent a while trying to get simp to do this, but Mario was always adamant that this wasn't simps job, and then Rob Lewis I think supervised an UG or masters project which became norm_cast. Note that Nat.cast_inj is tagged @[norm_cast] in the source.

[Chris Wong]

Is norm_cast inspired by another proof assistant, or is it a Lean original?

[Chris Wong]

The conclusion of this paper seems to imply the latter – https://lean-forward.github.io/norm_cast/norm_cast.pdf