-- Module: Mathlib.Algebra.Homology.AlternatingConst
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
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))
                    ⋯ :
                  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))
                    ⋯ :
                  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)
⊢ 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)

Tactic:
ext