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

Tactic:
refine Cofork.ext (Iso.refl _) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cofork.ext