C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ιCoprod s.N A ≫ map X s.ι Δ₁) ≫ X.map p = ιCoprod s.N (IndexSet.epiComp A p) ≫ map X s.ι Δ₂
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ ιSummand s A ≫ X.map p = ιSummand s (IndexSet.epiComp A p)
dsimp [ιSummand]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len { as := A }.as.fst.unop) ≫ X.map (IndexSet.e { as := A }.as).op) ≫ X.map p =
    ι s (len { as := IndexSet.epiComp A p }.as.fst.unop) ≫ X.map (IndexSet.e { as := IndexSet.epiComp A p }.as).op
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ιCoprod s.N A ≫ map X s.ι Δ₁) ≫ X.map p = ιCoprod s.N (IndexSet.epiComp A p) ≫ map X s.ι Δ₂
erw [colimit.ι_desc, colimit.ι_desc, Cofan.mk_ι_app, Cofan.mk_ι_app]
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len A.fst.unop) ≫ X.map (↑A.snd).op) ≫ X.map p = ι s (len A.fst.unop) ≫ X.map (p.unop ≫ ↑A.snd).op
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len { as := A }.as.fst.unop) ≫ X.map (IndexSet.e { as := A }.as).op) ≫ X.map p =
    ι s (len { as := IndexSet.epiComp A p }.as.fst.unop) ≫ X.map (IndexSet.e { as := IndexSet.epiComp A p }.as).op
dsimp only [IndexSet.epiComp, IndexSet.e]
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
Δ₁ Δ₂ : SimplexCategoryᵒᵖ
A : IndexSet Δ₁
p : Δ₁ ⟶ Δ₂
inst✝ : Epi p.unop
⊢ (ι s (len A.fst.unop) ≫ X.map (↑A.snd).op) ≫ X.map p = ι s (len A.fst.unop) ≫ X.map (p.unop ≫ ↑A.snd).op
rw [op_comp, X.map_comp, assoc, Quiver.Hom.op_unop]