-- 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
zero :
  Iso (C := ShortComplex.{v, u} C)
    (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.mk (X₁ := syzygies.{v, u} (X := over.{v, u} Z) (Projective.π Z)) (d (Projective.π Z)) (Projective.π Z)
      ⋯)
⊢ ShortComplex.Exact.{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)
        ⋯) ∧
    Epi.{v, u} (C := C) (X := HomologicalComplex.X.{v, u, 0} (ofComplex Z) 0) (Y := Z)
      (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:
refine (ShortComplex.exact_and_epi_g_iff_of_iso ?_).2
          ⟨exact_d_f (Projective.π Z), by dsimp; infer_instance⟩

Premises used: Iff.mpr, CategoryTheory.Projective.π, CategoryTheory.ShortComplex.exact_and_epi_g_iff_of_iso, And.intro, CategoryTheory.exact_d_f