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