English
For i ∈ Fin(n+1) and j ∈ Fin n, (j.predAbove i).predAbove (i.succAbove j) = j.
Русский
Для i ∈ Fin(n+1) и j ∈ Fin(n): (j.predAbove i).predAbove (i.succAbove j) = j.
LaTeX
$$$\forall i \in \mathrm{Fin}(n+1),\ \forall j \in \mathrm{Fin}(n),\ (j.predAbove i).predAbove (i.succAbove j) = j$$$
Lean4
theorem predAbove_predAbove_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
(j.predAbove i).predAbove (i.succAbove j) = j := by
cases j.castSucc.lt_or_le i with
| inl
h =>
rw [predAbove_of_castSucc_lt _ _ h, succAbove_of_castSucc_lt _ _ h, predAbove_of_le_castSucc, castPred_castSucc]
rwa [le_castSucc_iff, succ_pred]
| inr
h =>
rw [predAbove_of_le_castSucc _ _ h, succAbove_of_le_castSucc _ _ h, predAbove_of_castSucc_lt, pred_succ]
rwa [castSucc_castPred, ← le_castSucc_iff]
