English
Given h: n ≤ k, and i ∈ Fin k with hi ∈ Set.range(Fin.castLE h), the corresponding natural value via the inverse Equiv equals i.
Русский
Дано h: n ≤ k. Пусть i ∈ Fin k и i принадлежит образу Fin.castLE h; соответствующее число через обратное отображение равно i.
LaTeX
$$$\\forall {n k : \\mathbb{N}} (h : n \\le k) (i : \\mathrm{Fin}(k)) (hi : \\mathrm{Set}.instMembership.mem (\\mathrm{Set.range}(\\mathrm{Fin.castLE} h)) i),\\n ((\\mathrm{Equiv.ofInjective}(\\mathrm{Fin.castLE} h)).symm\\langle i, hi\\rangle : \\mathbb{N}) = i$$$
Lean4
@[simp]
theorem coe_of_injective_castLE_symm {n k : ℕ} (h : n ≤ k) (i : Fin k) (hi) :
((Equiv.ofInjective _ (castLE_injective h)).symm ⟨i, hi⟩ : ℕ) = i :=
by
rw [← coe_castLE h]
exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)
