English
Equality of mapped values is equivalent to equality of original ENat arguments: ENat.map Nat.cast m = ENat.map Nat.cast n iff m = n.
Русский
Равенство отображений равно равенству исходников: ENat.map Nat.cast m = ENat.map Nat.cast n эквивалентно m = n.
LaTeX
$$$$ \\mathrm{ENat.map}(\\mathrm{Nat.cast})\,m = \\mathrm{ENat.map}(\\mathrm{Nat.cast})\,n \\iff m = n $$$$
Lean4
@[simp]
theorem map_natCast_inj : m.map (Nat.cast : ℕ → α) = n.map Nat.cast ↔ m = n :=
map_natCast_injective.eq_iff