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