no goals
C : Type u_1
inst✝¹ : Category C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
Δ : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
⊢ Splitting.ιSummand S₁.s A ≫ Φ.F.app Δ = Hom.f Φ (len A.fst.unop) ≫ Splitting.ιSummand S₂.s A
erw [S₁.s.ιSummand_eq, S₂.s.ιSummand_eq, assoc, Φ.F.naturality, ← Φ.comm_assoc ]