-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero (goal)
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
⊢ (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) ⋯
have 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))
                sorry sorry).inv).obj
        (Preadditive.cokernelCoforkOfCofork
          (Cofork.ofπ (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (↾π₀.mk)) sorry))) ≫
    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))
                    sorry sorry).inv).obj
            (Preadditive.cokernelCoforkOfCofork
              (Cofork.ofπ (CategoryTheory.Functor.map (Functor.obj sigmaConst R) (↾π₀.mk)) sorry))).pt) =
  Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) sorry)
Tactic: refine Cofork.ext (Iso.refl _) ?_