Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ Cofork.π
        ((Cocone.precompose
              (parallelPair.ext
                  (-Iso.refl
                      ((parallelPair
                            ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                              (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                            0).obj
                        WalkingParallelPair.zero))
                  (Iso.refl
                    ((parallelPair
                          ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                            (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                          0).obj
                      WalkingParallelPair.one))
                  ⋯ ⋯).inv).obj
          (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))) ≫
      (Iso.refl
          ((Cocone.precompose
                  (parallelPair.ext
                      (-Iso.refl
                          ((parallelPair
                                ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                  (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                                0).obj
                            WalkingParallelPair.zero))
                      (Iso.refl
                        ((parallelPair
                              ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                              0).obj
                          WalkingParallelPair.one))
                      ⋯ ⋯).inv).obj
              (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))).pt).hom =
    Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
ext

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
x✝ : X _⦋0⦌
⊢ X.ιChainComplex x✝ ≫
      Cofork.π
          ((Cocone.precompose
                (parallelPair.ext
                    (-Iso.refl
                        ((parallelPair
                              ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                              0).obj
                          WalkingParallelPair.zero))
                    (Iso.refl
                      ((parallelPair
                            ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                              (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                            0).obj
                        WalkingParallelPair.one))
                    ⋯ ⋯).inv).obj
            (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))) ≫
        (Iso.refl
            ((Cocone.precompose
                    (parallelPair.ext
                        (-Iso.refl
                            ((parallelPair
                                  ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                    (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                                  0).obj
                              WalkingParallelPair.zero))
                        (Iso.refl
                          ((parallelPair
                                ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                  (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                                0).obj
                            WalkingParallelPair.one))
                        ⋯ ⋯).inv).obj
                (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))).pt).hom =
    X.ιChainComplex x✝ ≫ Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)