C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (↑Fin.castSucc i)) =
    X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.succ i))
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X i ≫ δ X (↑Fin.castSucc i) = δ X i ≫ δ X (Fin.succ i)
dsimp [δ]
no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (↑Fin.castSucc i)) =
    X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ (Fin.succ i))
simp only [← X.map_comp, SimplexCategory.δ_comp_δ_self]