-- 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
refine_2 :
  ∀ (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) ⋯)
⊢ 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) =
    Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
ext