-- Module: Mathlib.CategoryTheory.Abelian.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
⊢ Iso.hom
        (Iso.refl
          (ShortComplex.X₂.{v, u}
            (ShortComplex.mk (X₁ :=
              ShortComplex.X₂.{v, u}
                (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
                  (Functor.obj (CochainComplex.single₀ C) Z)))
              (X₂ :=
              ShortComplex.X₂.{v, u}
                (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
              (ShortComplex.Hom.τ₂
                (Functor.map (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
                  ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
                      (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
                        (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
                    (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
                        Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                          (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0)
                        (Injective.ι Z) ⋯ :
                      { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
                        Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                          (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0 }))))
              (ShortComplex.g
                (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
              ⋯))) ≫
      ShortComplex.g
        (ShortComplex.mk (X₂ := under.{v, u} Z) (X₃ := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (Injective.ι Z) (d (Injective.ι Z)) ⋯) =
    ShortComplex.g
        (ShortComplex.mk (X₁ :=
          ShortComplex.X₂.{v, u}
            (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
              (Functor.obj (CochainComplex.single₀ C) Z)))
          (X₂ :=
          ShortComplex.X₂.{v, u}
            (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
          (ShortComplex.Hom.τ₂
            (Functor.map (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
              ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
                  (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
                    (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
                (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
                    Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                      (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0)
                    (Injective.ι Z) ⋯ :
                  { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
                    Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                      (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0 }))))
          (ShortComplex.g
            (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
          ⋯) ≫
      Iso.hom
        (Iso.refl
          (ShortComplex.X₃.{v, u}
            (ShortComplex.mk (X₁ :=
              ShortComplex.X₂.{v, u}
                (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
                  (Functor.obj (CochainComplex.single₀ C) Z)))
              (X₂ :=
              ShortComplex.X₂.{v, u}
                (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
              (ShortComplex.Hom.τ₂
                (Functor.map (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
                  ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
                      (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
                        (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
                    (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
                        Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                          (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0)
                        (Injective.ι Z) ⋯ :
                      { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
                        Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
                          (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0 }))))
              (ShortComplex.g
                (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1) (ofCocomplex Z)))
              ⋯)))

Tactic:
simp [ofCocomplex]

Premises used: CategoryTheory.InjectiveResolution.ofCocomplex