-- Lean 4 proof step from Mathlib.Algebra.Homology.AlternatingConst (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 : C
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
      (Functor.obj ChainComplex.alternatingConst Y))
    (CategoryTheory.Functor.map (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (HomologicalComplex.Hom.isoOfComponents
                (fun (x : ℕ) ↦
                  Iso.refl
                    (HomologicalComplex.X.{v_1, u_1, 0}
                      (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
                ⋯ :
              Iso (C := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
                (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
                (Functor.obj ChainComplex.alternatingConst X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (HomologicalComplex.Hom.isoOfComponents
                (fun (x : ℕ) ↦
                  Iso.refl
                    (HomologicalComplex.X.{v_1, u_1, 0}
                      (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
                ⋯ :
              Iso (C := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
                (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
                (Functor.obj ChainComplex.alternatingConst X)))
          X) ≫
      CategoryTheory.Functor.map ChainComplex.alternatingConst f)
have h : ∀ (i : ℕ),
  Eq (α :=
    HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
        i ⟶
      HomologicalComplex.X.{v_1, u_1, 0} (Functor.obj ChainComplex.alternatingConst Y) i)
    (HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) f ≫
        Iso.hom
          ((fun (X : C) ↦
              (HomologicalComplex.Hom.isoOfComponents
                  (fun (x : ℕ) ↦
                    Iso.refl
                      (HomologicalComplex.X.{v_1, u_1, 0}
                        (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
                  sorry :
                Iso (C := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
                  (Functor.obj ChainComplex.alternatingConst X)))
            Y))
      i)
    (HomologicalComplex.Hom.f
      (Iso.hom
          ((fun (X : C) ↦
              (HomologicalComplex.Hom.isoOfComponents
                  (fun (x : ℕ) ↦
                    Iso.refl
                      (HomologicalComplex.X.{v_1, u_1, 0}
                        (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X) x))
                  sorry :
                Iso (C := HomologicalComplex.{v_1, u_1, 0} C (ComplexShape.down ℕ))
                  (Functor.obj (Functor.const SimplexCategoryᵒᵖ ⋙ alternatingFaceMapComplex C) X)
                  (Functor.obj ChainComplex.alternatingConst X)))
            X) ≫
        CategoryTheory.Functor.map ChainComplex.alternatingConst f)
      i)
Tactic: ext