English
Let p,i ∈ Fin(n+1) with i ≤ p and hp ≠ last n. Then (castPred p hp).predAbove i = castPred i (Fin.ne_of_lt (Fin.lt_of_le_of_lt h (Fin.lt_last_iff_ne_last.2 hp))).
Русский
Пусть p,i ∈ Fin(n+1) и i ≤ p и hp ≠ last n. Тогда (castPred p hp).predAbove i = castPred i (Fin.ne_of_lt (Fin.lt_of_le_of_lt h (Fin.lt_last_iff_ne_last.2 hp))).
LaTeX
$$$ \\forall p,i \\in \\mathrm{Fin}(n+1),\\ h:\\ i \\le p,\\ hp:\\ (p \\neq \\operatorname{last}~n) \\\\ :\\ (\\operatorname{castPred}~p~hp).predAbove i = \\operatorname{castPred}~i \\bigl( \\operatorname{Fin.ne\\_of\\_lt} \\bigl( \\operatorname{Fin.lt\\_of\\_le\\_of\\_lt} h \\ (\\operatorname{Fin.lt\\_last\\_iff\\_ne\\_last}.2 hp) \\bigr) \\bigr) $$$
Lean4
theorem predAbove_castPred_of_le (p i : Fin (n + 1)) (h : i ≤ p) (hp : p ≠ last n) :
(castPred p hp).predAbove i = castPred i (Fin.ne_of_lt <| Fin.lt_of_le_of_lt h <| Fin.lt_last_iff_ne_last.2 hp) :=
by rw [predAbove_of_le_castSucc _ _ (castSucc_castPred _ _ ▸ h)]
