English
For n, i, j with j.castSucc < i, we have δ_i.succ ∘ σ_j.castSucc = σ_j ∘ δ_i.
Русский
Для любых n, i, j такие, что j.castSucc < i, выполняется δ_i.succ ∘ σ_j.castSucc = σ_j ∘ δ_i.
LaTeX
$$$\\delta i.\\text{succ} \\circ \\sigma j.\\text{castSucc} = \\sigma j.\\text{castSucc} \\circ \\delta i$ при условии $j.castSucc < i$$$
Lean4
/-- The fourth simplicial identity -/
@[reassoc]
theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :
δ i.succ ≫ σ j.castSucc = σ j ≫ δ i := by
ext k : 3
dsimp [δ, σ]
rcases le_or_gt k i with (hik | hik)
· rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hik)]
rcases le_or_gt k (j.castSucc) with (hjk | hjk)
· rw [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hjk), Fin.castPred_castSucc,
Fin.predAbove_of_le_castSucc _ _ hjk, Fin.succAbove_of_castSucc_lt, Fin.castSucc_castPred]
rw [Fin.castSucc_castPred]
exact hjk.trans_lt H
· rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hjk), Fin.predAbove_of_castSucc_lt _ _ hjk,
Fin.succAbove_of_castSucc_lt, Fin.castSucc_pred_eq_pred_castSucc]
rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]
· rw [Fin.succAbove_of_le_castSucc _ _ (Fin.succ_le_castSucc_iff.mpr hik)]
have hjk := H.trans hik
rw [Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hjk.le),
Fin.pred_succ, Fin.succAbove_of_le_castSucc, Fin.succ_pred]
rwa [Fin.le_castSucc_pred_iff]
