English
For hmn: m ≤ n, a,b ∈ Fin m, castLE hmn a = castLE hmn b iff a = b.
Русский
Для hmn: m ≤ n, a,b ∈ Fin m, castLE hmn a = castLE hmn b тогда и только тогда a = b.
LaTeX
$$$\\forall {hmn : m \\le n},\\ a,b : \\mathrm{Fin}(m):\\; \\mathrm{castLE}\\ hmn\\ a = \\mathrm{castLE}\\ hmn\\ b \\iff a = b$$$
Lean4
@[simp]
theorem castLE_inj {hmn : m ≤ n} {a b : Fin m} : castLE hmn a = castLE hmn b ↔ a = b := by simp [Fin.ext_iff]