C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.succ i) ≫ σ X i = 𝟙 (X.obj [n])
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = Fin.succ i
⊢ δ X j ≫ σ X i = 𝟙 (X.obj [n])
subst H
no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 1)
⊢ δ X (Fin.succ i) ≫ σ X i = 𝟙 (X.obj [n])
rw [δ_comp_σ_succ]