C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X (↑Fin.castSucc i) ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = ↑Fin.castSucc i
⊢ δ X j ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
subst H
no goals
C : Type u
inst✝ : Category C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ δ X (↑Fin.castSucc i) ≫ δ X i = δ X (Fin.succ i) ≫ δ X i
rw [δ_comp_δ_self]