C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ (Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (Splitting.iso (splitting K) Δ).hom) ≫ (obj K).map θ =
    Termwise.mapMono K i ≫
      Sigma.ι (Splitting.summand (splitting K).N Δ'.unop.op) (Splitting.IndexSet.mk e) ≫
        (Splitting.iso (splitting K) Δ'.unop.op).hom
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Splitting.ιSummand (splitting K) A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ Splitting.ιSummand (splitting K) (Splitting.IndexSet.mk e)
dsimp only [SimplicialObject.Splitting.ιSummand, SimplicialObject.Splitting.ιCoprod]
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ Sigma.ι (Splitting.summand (splitting K).N Δ'.unop.op) (Splitting.IndexSet.mk e)
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ (Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (Splitting.iso (splitting K) Δ).hom) ≫ (obj K).map θ =
    Termwise.mapMono K i ≫
      Sigma.ι (Splitting.summand (splitting K).N Δ'.unop.op) (Splitting.IndexSet.mk e) ≫
        (Splitting.iso (splitting K) Δ'.unop.op).hom
simp only [assoc, Γ₀.splitting_iso_hom_eq_id, id_comp, comp_id]
no goals
C : Type u_2
inst✝⁴ : Category C
inst✝³ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ'✝ Δ''✝ : SimplexCategory
inst✝² : HasFiniteCoproducts C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : Δ'.unop ⟶ Δ''
i : Δ'' ⟶ A.fst.unop
inst✝¹ : Epi e
inst✝ : Mono i
fac : e ≫ i = θ.unop ≫ Splitting.IndexSet.e A
⊢ Sigma.ι (Splitting.summand (splitting K).N Δ) A ≫ (obj K).map θ =
    Termwise.mapMono K i ≫ Sigma.ι (Splitting.summand (splitting K).N Δ'.unop.op) (Splitting.IndexSet.mk e)
exact Γ₀.Obj.map_on_summand₀ K A fac