C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ((ιCoprod s.N A ≫ map X s.ι Δ) ≫
      inv (map X s.ι Δ) ≫
        Sigma.desc fun B =>
          if h : B = A then eqToHom (_ : summand s.N Δ B = N s (SimplexCategory.len A.fst.unop)) else 0) =
    𝟙 (N s (SimplexCategory.len A.fst.unop))
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ πSummand s A = 𝟙 (N s (SimplexCategory.len A.fst.unop))
dsimp [ιSummand, πSummand]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (ιCoprod s.N A ≫
      Sigma.desc fun B =>
        if h : B = A then eqToHom (_ : summand s.N Δ B = N s (SimplexCategory.len A.fst.unop)) else 0) =
    𝟙 (N s (SimplexCategory.len A.fst.unop))
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ((ιCoprod s.N A ≫ map X s.ι Δ) ≫
      inv (map X s.ι Δ) ≫
        Sigma.desc fun B =>
          if h : B = A then eqToHom (_ : summand s.N Δ B = N s (SimplexCategory.len A.fst.unop)) else 0) =
    𝟙 (N s (SimplexCategory.len A.fst.unop))
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 : IndexSet Δ
⊢ (if h : { as := A }.as = A then eqToHom (_ : summand s.N Δ { as := A }.as = N s (SimplexCategory.len A.fst.unop))
    else 0) =
    𝟙 (N s (SimplexCategory.len A.fst.unop))
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (ιCoprod s.N A ≫
      Sigma.desc fun B =>
        if h : B = A then eqToHom (_ : summand s.N Δ B = N s (SimplexCategory.len A.fst.unop)) else 0) =
    𝟙 (N s (SimplexCategory.len A.fst.unop))
erw [colimit.ι_desc, Cofan.mk_ι_app]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (if h : A = A then 𝟙 (N s (SimplexCategory.len A.fst.unop)) else 0) = 𝟙 (N s (SimplexCategory.len A.fst.unop))
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (if h : { as := A }.as = A then eqToHom (_ : summand s.N Δ { as := A }.as = N s (SimplexCategory.len A.fst.unop))
    else 0) =
    𝟙 (N s (SimplexCategory.len A.fst.unop))
dsimp
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (if h : A = A then 𝟙 (N s (SimplexCategory.len A.fst.unop)) else 0) = 𝟙 (N s (SimplexCategory.len A.fst.unop))
simp only [dite_eq_ite, ite_true]