English
For x ∈ { x ∈ Fin(n+1) | x ≠ Fin.last n }, the inverse of finSuccAboveEquiv at p = Fin.last n yields Fin.castLT(x.1, val_lt_last(x.2)).
Русский
Для x ∈ { x ∈ Fin(n+1) | x ≠ Fin.last n }, образ обратной функции finSuccAboveEquiv(Fin.last n) aplicado к x равен Fin.castLT(x.1, val_lt_last(x.2)).
LaTeX
$$$$ \\forall x : \\{ x : \\mathrm{Fin}(n+1) \\mid x \\neq \\mathrm{Fin.last}(n) \\},\\; (\\mathrm{finSuccAboveEquiv}(\\mathrm{Fin.last}(n))).\\mathrm{symm} x = \\mathrm{Fin.castLT}(x.1, \\mathrm{Fin.val\\_lt\\_last}(x.2)). $$$$
Lean4
theorem finSuccAboveEquiv_symm_apply_last (x : { x : Fin (n + 1) // x ≠ Fin.last n }) :
(finSuccAboveEquiv (Fin.last n)).symm x = Fin.castLT x.1 (Fin.val_lt_last x.2) :=
by
rw [← Option.some_inj]
simp [finSuccAboveEquiv]
