-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
⊢ QuasiIsoAt.{v, u, 0} (ι := ℕ) (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((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 }))
    0
have zero : ShortComplex.Exact.{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) sorry :
              { 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)))
      sorry) ∧
  Mono.{v, u} (X :=
    ShortComplex.X₂.{v, u}
      (Functor.obj (HomologicalComplex.shortComplexFunctor' C (ComplexShape.up ℕ) 0 0 1)
        (Functor.obj (CochainComplex.single₀ C) Z)))
    (Y :=
    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) sorry :
            { 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 }))))
Tactic: rw [CochainComplex.quasiIsoAt₀_iff, ShortComplex.quasiIso_iff_of_zeros]