no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
hj : j = 0
⊢ False
simp only [hj, Fin.not_lt_zero] at H
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) =
    X.map (SimplexCategory.δ (Fin.pred j (_ : j = 0 → False))) ≫ X.map (SimplexCategory.δ (↑Fin.castSucc i))
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ δ X i ≫ δ X j = δ X (Fin.pred j (_ : j = 0 → False)) ≫ δ X (↑Fin.castSucc i)
dsimp [δ]
no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j) =
    X.map (SimplexCategory.δ (Fin.pred j (_ : j = 0 → False))) ≫ X.map (SimplexCategory.δ (↑Fin.castSucc i))
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_δ' H]