no goals
C : Type u_2
inst✝³ : Category C
inst✝² : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ'' : SimplexCategory
inst✝¹ : HasFiniteCoproducts C
Δ Δ' : SimplexCategory
e : Δ' ⟶ Δ
inst✝ : Epi e
⊢ Splitting.ιSummand (splitting K) (Splitting.IndexSet.id Δ.op) ≫ (obj K).map e.op =
    Splitting.ιSummand (splitting K) (Splitting.IndexSet.mk e)
simpa only [Γ₀.Obj.map_on_summand K (Splitting.IndexSet.id (op Δ)) e.op
    (rfl : e ≫ 𝟙 Δ = e ≫ 𝟙 Δ),
  Γ₀.Obj.Termwise.mapMono_id] using id_comp _