-- 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
⊢ 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) ⋯)
have 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))
                    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) =
    X.ιChainComplex x ≫ Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) sorry)
Tactic: ext