English
The equality of the composition of the constant map with a subinterval, giving a matched endpoint shift as described by the lemma const_subinterval_eq.
Русский
Согласованность композиции константного отображения с подинтервалом, выражаемая леммой const_subinterval_eq.
LaTeX
$$$\Delta^0 . const \Delta^l i \circ \mathrm{subinterval}(j,l,h) = \Delta^0 . const \Delta^n \langle j+i.1, \cdots \rangle$$$
Lean4
/-- The first part of the third simplicial identity -/
@[reassoc]
theorem δ_comp_σ_self {n} {i : Fin (n + 1)} : δ (Fin.castSucc i) ≫ σ i = 𝟙 ⦋n⦌ :=
by
rcases i with ⟨i, hi⟩
ext ⟨j, hj⟩
simp? at hj says simp only [len_mk] at hj
dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
simp only [Fin.lt_iff_val_lt_val, Fin.dite_val, Fin.ite_val, Fin.coe_pred]
split_ifs
any_goals simp
all_goals cutsat
