-- Lean 4 proof step from Mathlib.AlgebraicTopology.AlternatingFaceMapComplex (goal)
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
⊢ 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)
have 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⦌)) sorry))
    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⦌)) sorry) ≫
      CategoryTheory.Functor.map (SimplicialObject.Augmented.point ⋙ ChainComplex.single₀ C) f)
    0)
Tactic: apply HomologicalComplex.to_single_hom_ext