-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Projective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughProjectives.{v, u} C
Z : C
zero :
  ShortComplex.Exact.{v, u}
      (ShortComplex.mk (X₁ :=
        ShortComplex.X₁.{v, u}
          (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)))
        (X₃ :=
        ShortComplex.X₂.{v, u}
          (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
            (Functor.obj (ChainComplex.single₀ C) Z)))
        (ShortComplex.f
          (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)))
        (ShortComplex.Hom.τ₂
          (Functor.map (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
            ((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 }))))
        ⋯) ∧
    Epi.{v, u} (X :=
      ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)))
      (Y :=
      ShortComplex.X₂.{v, u}
        (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (ChainComplex.single₀ C) Z)))
      (ShortComplex.Hom.τ₂
        (Functor.map (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0)
          ((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 }))))
⊢ QuasiIsoAt.{v, u, 0} (ι := ℕ) (C := C) (c := ComplexShape.down ℕ) (K := ofComplex Z) (L :=
    Functor.obj (ChainComplex.single₀ C) Z)
    ((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
have zero₁ : Eq.{v + 1} (α :=
  ShortComplex.X₂.{v, u}
      (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)) ⟶
    ShortComplex.X₃.{v, u}
      (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z)))
  (ShortComplex.g (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0) (ofComplex Z))) 0
Tactic: rw [ChainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros']