-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
X : SSet
R : C
x : X _⦋0⦌
⊢ X.ιChainComplex x ≫
      Cofork.π
          ((Cocone.precompose
                (parallelPair.ext
                    (-Iso.refl
                        ((parallelPair
                              (HSub.hSub (α :=
                                Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                                  Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                                (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                                (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                              0).obj
                          WalkingParallelPair.zero))
                    (Iso.refl
                      ((parallelPair
                            (HSub.hSub (α :=
                              Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                                Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                              (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                            0).obj
                        WalkingParallelPair.one))
                    ⋯ ⋯).inv).obj
            (Preadditive.cokernelCoforkOfCofork
              (Cofork.ofπ (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (↾π₀.mk)) ⋯))) ≫
        Iso.hom
          (Iso.refl
            ((Cocone.precompose
                    (parallelPair.ext
                        (-Iso.refl
                            ((parallelPair
                                  (HSub.hSub (α :=
                                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R)
                                        (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                                      Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                                    (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                                  0).obj
                              WalkingParallelPair.zero))
                        (Iso.refl
                          ((parallelPair
                                (HSub.hSub (α :=
                                  Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R)
                                      (X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) ⟶
                                    Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) (X _⦋0⦌))
                                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 1))
                                  (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (SimplicialObject.δ X 0)))
                                0).obj
                            WalkingParallelPair.one))
                        ⋯ ⋯).inv).obj
                (Preadditive.cokernelCoforkOfCofork
                  (Cofork.ofπ (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (↾π₀.mk)) ⋯))).pt) =
    X.ιChainComplex x ≫ Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
simp [chainComplex, SSet.chainComplexFunctor, π₀.fromChainComplexXZero]

Premises used: SSet.chainComplexFunctor, SSet.π₀.fromChainComplexXZero, SSet.chainComplex