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