C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op ≫ f.app Δ =
    ι s (len A.fst.unop) ≫ f.app [len A.fst.unop].op ≫ Y.map (IndexSet.e A).op
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ιSummand s A ≫ f.app Δ = φ s f (len A.fst.unop) ≫ Y.map (IndexSet.e A).op
simp only [ιSummand_eq_assoc, φ, assoc]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
s : Splitting X
f : X ⟶ Y
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ ι s (len A.fst.unop) ≫ X.map (IndexSet.e A).op ≫ f.app Δ =
    ι s (len A.fst.unop) ≫ f.app [len A.fst.unop].op ≫ Y.map (IndexSet.e A).op
erw [NatTrans.naturality]