-- 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 (α :=
    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)
have hfg : Eq (α := X.left _⦋0⦌ ⟶ Y.right)
  (f.left.app (op ⦋0⦌) ≫
    HomologicalComplex.Hom.f
      ((Equiv.symm (ChainComplex.toSingle₀Equiv (Functor.obj (alternatingFaceMapComplex C) Y.left) Y.right) :
          (a : { f : Y.left _⦋0⦌ ⟶ Y.right // ((alternatingFaceMapComplex C).obj Y.left).d 1 0 ≫ f = 0 }) →
            (alternatingFaceMapComplex C).obj Y.left ⟶ (ChainComplex.single₀ C).obj Y.right)
        (Subtype.mk (p := fun (f : Y.left _⦋0⦌ ⟶ Y.right) ↦
          Eq (α := Y.left _⦋1⦌ ⟶ Y.right)
            (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) Y.left) 1 0 ≫ f : Y.left _⦋1⦌ ⟶ Y.right)
            (0 :
              HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) Y) 1 ⟶
                Functor.obj SimplicialObject.Augmented.point Y))
          (Y.hom.app (op ⦋0⦌)) sorry))
      0)
  (CategoryStruct.comp (Y := X.right)
    (HomologicalComplex.Hom.f
      ((Equiv.symm (ChainComplex.toSingle₀Equiv (Functor.obj (alternatingFaceMapComplex C) X.left) X.right) :
          (a : { f : X.left _⦋0⦌ ⟶ X.right // ((alternatingFaceMapComplex C).obj X.left).d 1 0 ≫ f = 0 }) →
            (alternatingFaceMapComplex C).obj X.left ⟶ (ChainComplex.single₀ C).obj X.right)
        (Subtype.mk (p := fun (f : X.left _⦋0⦌ ⟶ X.right) ↦
          Eq (α := X.left _⦋1⦌ ⟶ X.right)
            (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) X.left) 1 0 ≫ f : X.left _⦋1⦌ ⟶ X.right)
            (0 :
              HomologicalComplex.X (Functor.obj (SimplicialObject.Augmented.drop ⋙ alternatingFaceMapComplex C) X) 1 ⟶
                Functor.obj SimplicialObject.Augmented.point X))
          (X.hom.app (op ⦋0⦌)) sorry))
      0)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (ChainComplex.single₀ C) f.right) 0))
Tactic: dsimp