case h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝¹ : Discrete (Splitting.IndexSet Δ✝)
A✝ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝ : Discrete (Splitting.IndexSet Δ.op)
A : Splitting.IndexSet Δ.op
⊢ colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ.op))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K [n].op) (Splitting.IndexSet.id [n].op)) Δ.op =
    colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ.op))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ.op)
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ : SimplexCategoryᵒᵖ
x✝ : Discrete (Splitting.IndexSet Δ)
A : Splitting.IndexSet Δ
⊢ colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K [n].op) (Splitting.IndexSet.id [n].op)) Δ =
    colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ)
induction' Δ using Opposite.rec' with Δ
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K [n].op) (Splitting.IndexSet.id [n].op)) [n].op =
    colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op)
case h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝¹ : Discrete (Splitting.IndexSet Δ✝)
A✝ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝ : Discrete (Splitting.IndexSet Δ.op)
A : Splitting.IndexSet Δ.op
⊢ colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ.op))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K [n].op) (Splitting.IndexSet.id [n].op)) Δ.op =
    colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ.op))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) Δ.op)
induction' Δ using SimplexCategory.rec with n
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ (colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      Sigma.desc fun A =>
        Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op)
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ colimit.ι (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op))
        { as := A } ≫
      Splitting.map (obj K) (fun n => Sigma.ι (Obj.summand K [n].op) (Splitting.IndexSet.id [n].op)) [n].op =
    colimit.ι
        (Discrete.functor (Splitting.summand (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op))
        { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op)
dsimp [Splitting.map]
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op)
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ (colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      Sigma.desc fun A =>
        Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op)
simp only [colimit.ι_desc, Cofan.mk_ι_app, Γ₀.obj_map]
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ Sigma.ι (Obj.summand K [n].op)
      (Splitting.IndexSet.mk
        (Splitting.IndexSet.e
          { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } })) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst))
      { as := { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } } }
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ Sigma.ι (Obj.summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ Obj.map K (Splitting.IndexSet.e A).op =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst)) { as := A } ≫
      𝟙 (Splitting.coprod (fun n => Obj.summand K [n].op (Splitting.IndexSet.id [n].op)) [n].op)
erw [Γ₀.Obj.map_on_summand₀ K (SimplicialObject.Splitting.IndexSet.id A.1)
    (show A.e ≫ 𝟙 _ = A.e.op.unop ≫ 𝟙 _ by rfl),
  Γ₀.Obj.Termwise.mapMono_id, A.ext', id_comp, comp_id]
no goals
case h.h
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ Sigma.ι (Obj.summand K [n].op)
      (Splitting.IndexSet.mk
        (Splitting.IndexSet.e
          { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } })) =
    colimit.ι (Discrete.functor fun A => Obj.summand K A.fst (Splitting.IndexSet.id A.fst))
      { as := { fst := A.fst, snd := { val := Splitting.IndexSet.e A, property := (_ : Epi ↑A.snd) } } }
rfl
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : Preadditive C
K K' : ChainComplex C ℕ
f : K ⟶ K'
Δ✝¹ Δ' Δ'' : SimplexCategory
inst✝ : HasFiniteCoproducts C
Δ✝ : SimplexCategoryᵒᵖ
x✝² : Discrete (Splitting.IndexSet Δ✝)
A✝¹ : Splitting.IndexSet Δ✝
Δ : SimplexCategory
x✝¹ : Discrete (Splitting.IndexSet Δ.op)
A✝ : Splitting.IndexSet Δ.op
n : ℕ
x✝ : Discrete (Splitting.IndexSet [n].op)
A : Splitting.IndexSet [n].op
⊢ Splitting.IndexSet.e A ≫ 𝟙 A.fst.unop = (Splitting.IndexSet.e A).op.unop ≫ 𝟙 A.fst.unop.op.unop
rfl