English
A variant of the fourth simplicial identity: for i, j with j.succ < i, δ_i.succ ∘ σ_j.castSucc = σ_j.castLT ∘ δ_i.pred, adjusting indices via castLT.
Русский
Вариант четвертой симпликс идентичности: при j.succ < i имеем δ_i.succ ∘ σ_j.castSucc = σ_j.castLT ∘ δ_i.pred, с корректировкой индексов через castLT.
LaTeX
$$$\\\\forall n \\\\in \\\\mathbb{N}, \ i \\\\in \\\\mathrm{Fin}(n+3), \ j \\\\in \\\\mathrm{Fin}(n+2), \\\\text{with } (H: j.succ < i) \\\\Rightarrow \ δ_i \\\\circ \sigma_j = \\\\sigma (j.castLT( (\\\\text{add\_lt\_add\_iff\_right } 1).mp (lt\_of\_lt\_of\_le H i.is\_le ))) \\\\circ \ δ_i.pred( \\\\text{??} ).$$$
Lean4
/-- The fifth simplicial identity -/
@[reassoc]
theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) : σ (Fin.castSucc i) ≫ σ j = σ j.succ ≫ σ i :=
by
ext k : 3
dsimp [σ]
cases k using Fin.lastCases with
| last => simp only [len_mk, Fin.predAbove_right_last]
| cast k =>
cases k using Fin.cases with
| zero => simp
| succ k =>
rcases le_or_gt i k with (h | h)
· simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _
(Fin.castSucc_lt_castSucc_iff.mpr (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
Fin.succ_predAbove_succ]
rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
rcases le_or_gt k j with (hkj | hkj)
· rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj), Fin.castPred_castSucc]
· rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj), Fin.le_pred_iff,
Fin.succ_le_castSucc_iff]
exact H.trans_lt hkj
· simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _
(Fin.castSucc_le_castSucc_iff.mpr (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ←
Fin.succ_castSucc, Fin.succ_predAbove_succ]
rw [Fin.predAbove_of_le_castSucc _ k.castSucc (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)),
Fin.predAbove_of_le_castSucc _ k.succ (Fin.succ_le_castSucc_iff.mpr h)]
