English
castSucc commutes with succAbove: (i.castSucc).succAbove(j.castSucc) = (i.succAbove(j)).castSucc.
Русский
castSucc коммутирует с succAbove: (i.castSucc).succAbove(j.castSucc) = (i.succAbove(j)).castSucc.
LaTeX
$$$\forall i: \mathrm{Fin}(n+1),\forall j: \mathrm{Fin} n,\ i.castSucc.succAbove(j.castSucc) = (i.succAbove(j)).castSucc.$$$
Lean4
/-- `castSucc` commutes with `succAbove`. -/
@[simp]
theorem castSucc_succAbove_castSucc {n : ℕ} {i : Fin (n + 1)} {j : Fin n} :
i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc :=
by
rcases i.le_or_gt (castSucc j) with (h | h)
· rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]
· rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]
