English
Let p,i ∈ Fin(n+1) and h: i < p. Then (pred p (Fin.ne_zero_of_lt h)).predAbove i = castPred i (Fin.ne_last_of_lt h).
Русский
Пусть p,i ∈ Fin(n+1) и h: i < p. Тогда (pred p (Fin.ne_zero_of_lt h)).predAbove i = castPred i (Fin.ne_last_of_lt h).
LaTeX
$$$ \\forall p,i \\in \\mathrm{Fin}(n+1),\\ h:\\ i < p \\\\ :\\ (\\operatorname{pred}~p~(\\operatorname{Fin.ne\\_zero\\_of\\_lt} h)).predAbove(i) = \\operatorname{castPred} i (\\operatorname{Fin.ne\\_last\\_of\\_lt} h) $$$
Lean4
theorem predAbove_zero [NeZero n] {i : Fin (n + 1)} : predAbove (0 : Fin n) i = if hi : i = 0 then 0 else i.pred hi :=
by
split_ifs with hi
· rw [hi, predAbove_right_zero]
· rw [predAbove_zero_of_ne_zero hi]
