C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ((ιCoprod s.N A ≫ map X s.ι Δ) ≫
      inv (map X s.ι Δ) ≫
        Sigma.desc fun B_1 =>
          if h : B_1 = B then eqToHom (_ : summand s.N Δ B_1 = N s (SimplexCategory.len B.fst.unop)) else 0) =
    0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ιSummand s A ≫ πSummand s B = 0
dsimp [ιSummand, πSummand]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (ιCoprod s.N A ≫
      Sigma.desc fun B_1 =>
        if h : B_1 = B then eqToHom (_ : summand s.N Δ B_1 = N s (SimplexCategory.len B.fst.unop)) else 0) =
    0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ((ιCoprod s.N A ≫ map X s.ι Δ) ≫
      inv (map X s.ι Δ) ≫
        Sigma.desc fun B_1 =>
          if h : B_1 = B then eqToHom (_ : summand s.N Δ B_1 = N s (SimplexCategory.len B.fst.unop)) else 0) =
    0
simp only [summand, assoc, IsIso.hom_inv_id_assoc]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (if h : { as := A }.as = B then eqToHom (_ : summand s.N Δ { as := A }.as = N s (SimplexCategory.len B.fst.unop))
    else 0) =
    0
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (ιCoprod s.N A ≫
      Sigma.desc fun B_1 =>
        if h : B_1 = B then eqToHom (_ : summand s.N Δ B_1 = N s (SimplexCategory.len B.fst.unop)) else 0) =
    0
erw [colimit.ι_desc, Cofan.mk_ι_app]
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (if h : { as := A }.as = B then eqToHom (_ : summand s.N Δ { as := A }.as = N s (SimplexCategory.len B.fst.unop))
    else 0) =
    0
exact dif_neg h.symm