English
For i ∈ Fin(n+2), predAbove (last n) i equals last n if i = last(n+1), otherwise i.castPred hi for hi expressing i ≠ last(n+1).
Русский
Для i ∈ Fin(n+2) predAbove (last n) i равно last n, если i = last(n+1), иначе i.castPred hi, где hi выражает i ≠ last(n+1).
LaTeX
$$$ \\forall n, i \\in \\mathrm{Fin}(n+2),\\ predAbove(\\operatorname{last} n,i) = \\begin{cases} \\operatorname{last} n, & i = \\operatorname{last}(n+1), \\\\ i.castPred(hi), & i \\neq \\operatorname{last}(n+1) \\end{cases} $$$
Lean4
theorem predAbove_last_apply {i : Fin (n + 2)} :
predAbove (last n) i = if hi : i = last _ then last _ else i.castPred hi :=
by
split_ifs with hi
· rw [hi, predAbove_right_last]
· rw [predAbove_last_of_ne_last hi]
