C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιCoprod s.N A ≫ (iso s Δ).hom = ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A = ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
dsimp only [ιSummand, Iso.hom]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιCoprod s.N A ≫ (iso s Δ).hom = ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op
erw [colimit.ι_desc, Cofan.mk_ι_app]