no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject 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 : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))) ≫
      X.map (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False)))
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ δ X i ≫ σ X j = σ X (Fin.castLT j (_ : ↑j < n + 1)) ≫ δ X (Fin.pred i (_ : i = 0 → False))
dsimp [δ, σ]
no goals
C : Type u
inst✝ : Category C
X : CosimplicialObject C
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : Fin.succ j < i
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ (Fin.castLT j (_ : ↑j < n + 1))) ≫
      X.map (SimplexCategory.δ (Fin.pred i (_ : i = 0 → False)))
simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_gt' H]