C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.castLT i (_ : ↑i < n + 2))) ≫ X.map (SimplexCategory.δ (Fin.succ j)) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ δ X (Fin.castLT i (_ : ↑i < n + 2)) ≫ δ X (Fin.succ j) = δ X j ≫ δ X i
dsimp [δ]
no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ X.map (SimplexCategory.δ (Fin.castLT i (_ : ↑i < n + 2))) ≫ X.map (SimplexCategory.δ (Fin.succ j)) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i)
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ'' H]