-- Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
⊢ Iso.hom
        (Iso.refl
          (ShortComplex.X₁.{v, u}
            (ShortComplex.mk (X₁ := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1) (X₂ :=
              HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0) (X₃ := Z) (HomologicalComplex.d (ofComplex Z) 1 0)
              (HomologicalComplex.Hom.f
                  ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
                      (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
                        ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
                    (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
                        Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
                          (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
                        (Projective.π Z) ⋯ :
                      { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
                        Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
                          (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0 }))
                  0 :
                HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶
                  HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Z) 0)
              ⋯))) ≫
      ShortComplex.f
        (ShortComplex.mk (X₁ := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z))
          (Projective.π Z) ⋯) =
    ShortComplex.f
        (ShortComplex.mk (X₁ := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1) (X₂ :=
          HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0) (X₃ := Z) (HomologicalComplex.d (ofComplex Z) 1 0)
          (HomologicalComplex.Hom.f
              ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
                  (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
                    ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
                (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
                    Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
                      (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
                    (Projective.π Z) ⋯ :
                  { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
                    Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
                      (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0 }))
              0 :
            HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶
              HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Z) 0)
          ⋯) ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.X₂.{v, u}
            (ShortComplex.mk (X₁ := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1) (X₂ :=
              HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0) (X₃ := Z) (HomologicalComplex.d (ofComplex Z) 1 0)
              (HomologicalComplex.Hom.f
                  ((Equiv.symm (ChainComplex.toSingle₀Equiv (ofComplex Z) Z) :
                      (a : { f : (ofComplex Z).X 0 ⟶ Z // (ofComplex Z).d 1 0 ≫ f = 0 }) →
                        ofComplex Z ⟶ (ChainComplex.single₀ C).obj Z)
                    (Subtype.mk (p := fun (f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z) ↦
                        Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
                          (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0)
                        (Projective.π Z) ⋯ :
                      { f : HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶ Z //
                        Eq (α := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 1 ⟶ Z)
                          (HomologicalComplex.d (ofComplex Z) 1 0 ≫ f) 0 }))
                  0 :
                HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0 ⟶
                  HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Z) 0)
              ⋯)))

Tactic:
simp [ofComplex]

Premises used: CategoryTheory.ProjectiveResolution.ofComplex