-- Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X Y : SimplicialObject.Augmented.{v_1, u_1} C
f : X ⟶ Y
hfg :
  Eq (α :=
    HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
      HomologicalComplex.X.{v_1, u_1, 0}
        (Functor.obj (HomologicalComplex.single C (ComplexShape.down ℕ) 0)
          (Functor.obj SimplicialObject.Augmented.point Y))
        0)
    (HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) f ≫
        (Equiv.symm
              (ChainComplex.toSingle₀Equiv
                (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y)
                (Functor.obj SimplicialObject.Augmented.point Y)) :
            (a :
                { f :
                  ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).X 0 ⟶
                    SimplicialObject.Augmented.point.obj Y //
                  ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).d 1 0 ≫ f = 0 }) →
              (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y ⟶
                (ChainComplex.single₀ C).obj (SimplicialObject.Augmented.point.obj Y))
          (Subtype.mk (p :=
            fun
              (f :
                HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 0 ⟶
                  Functor.obj SimplicialObject.Augmented.point Y) ↦
            Eq (α :=
              HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 1 ⟶
                Functor.obj SimplicialObject.Augmented.point Y)
              (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 1
                  0 ≫
                f)
              0)
            (Y.hom.app (op ⦋0⦌)) ⋯))
      0)
    (HomologicalComplex.Hom.f
      ((Equiv.symm
              (ChainComplex.toSingle₀Equiv
                (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X)
                (Functor.obj SimplicialObject.Augmented.point X)) :
            (a :
                { f :
                  ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).X 0 ⟶
                    SimplicialObject.Augmented.point.obj X //
                  ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).d 1 0 ≫ f = 0 }) →
              (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X ⟶
                (ChainComplex.single₀ C).obj (SimplicialObject.Augmented.point.obj X))
          (Subtype.mk (p :=
            fun
              (f :
                HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
                  Functor.obj SimplicialObject.Augmented.point X) ↦
            Eq (α :=
              HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
                Functor.obj SimplicialObject.Augmented.point X)
              (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1
                  0 ≫
                f)
              0)
            (X.hom.app (op ⦋0⦌)) ⋯) ≫
        CategoryTheory.Functor.map (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) f)
      0)
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X)
      (Functor.obj (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) Y))
    (CategoryTheory.Functor.map (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) f ≫
      (Equiv.symm
            (ChainComplex.toSingle₀Equiv (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y)
              (Functor.obj SimplicialObject.Augmented.point Y)) :
          (a :
              { f :
                ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).X 0 ⟶
                  SimplicialObject.Augmented.point.obj Y //
                ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y).d 1 0 ≫ f = 0 }) →
            (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj Y ⟶
              (ChainComplex.single₀ C).obj (SimplicialObject.Augmented.point.obj Y))
        (Subtype.mk (p :=
          fun
            (f :
              HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 0 ⟶
                Functor.obj SimplicialObject.Augmented.point Y) ↦
          Eq (α :=
            HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 1 ⟶
              Functor.obj SimplicialObject.Augmented.point Y)
            (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 1 0 ≫
              f)
            0)
          (Y.hom.app (op ⦋0⦌)) ⋯))
    ((Equiv.symm
            (ChainComplex.toSingle₀Equiv (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X)
              (Functor.obj SimplicialObject.Augmented.point X)) :
          (a :
              { f :
                ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).X 0 ⟶
                  SimplicialObject.Augmented.point.obj X //
                ((SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X).d 1 0 ≫ f = 0 }) →
            (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C).obj X ⟶
              (ChainComplex.single₀ C).obj (SimplicialObject.Augmented.point.obj X))
        (Subtype.mk (p :=
          fun
            (f :
              HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 0 ⟶
                Functor.obj SimplicialObject.Augmented.point X) ↦
          Eq (α :=
            HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
              Functor.obj SimplicialObject.Augmented.point X)
            (HomologicalComplex.d (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 0 ≫
              f)
            0)
          (X.hom.app (op ⦋0⦌)) ⋯) ≫
      CategoryTheory.Functor.map (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) f)

Tactic:
apply HomologicalComplex.to_single_hom_ext

Premises used: HomologicalComplex.to_single_hom_ext