-- Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasZeroMorphisms.{v, u} C
Z : C
I : InjectiveResolution.{v, u} Z
rw :
  CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt) 0)
      (Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt))
      (Iso.hom (isoHomologyπ₀ (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt)) ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≫
          CategoryStruct.comp (Y :=
            Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
              (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
            (Iso.hom
                (Iso.symm (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≪≫
                  Iso.trans (Y := homology I.cocomplex 0) (isoOfQuasiIsoAt I.ι 0)
                    (Iso.symm I.cocomplex.isoHomologyπ₀)) :
              I.kernelFork.pt ⟶
                Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
                  (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
            (Fork.ι (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) :
              Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
                  (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) ⟶
                I.cocomplex.X 0)) =
    CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt) 0)
      (Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt))
      (Iso.hom (isoHomologyπ₀ (Functor.obj (single C (ComplexShape.up ℕ) 0) I.kernelFork.pt)) ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≫ Fork.ι I.kernelFork)
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
        (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
      (Iso.hom
          (Iso.symm (singleObjHomologySelfIso (ComplexShape.up ℕ) 0 I.kernelFork.pt) ≪≫
            Iso.trans (Y := homology I.cocomplex 0) (isoOfQuasiIsoAt I.ι 0) (Iso.symm I.cocomplex.isoHomologyπ₀)) :
        I.kernelFork.pt ⟶
          Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
            (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯))
      (Fork.ι (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) :
        Cone.pt (F := parallelPair (X := I.cocomplex.X 0) (Y := I.cocomplex.X 1) (I.cocomplex.d 0 1) 0)
            (KernelFork.ofι (Z := cycles I.cocomplex 0) (iCycles I.cocomplex 0) ⋯) ⟶
          I.cocomplex.X 0) =
    Fork.ι I.kernelFork

Tactic:
rw [← cancel_epi (singleObjHomologySelfIso (ComplexShape.up ℕ) _ _).hom,
    ← cancel_epi (isoHomologyπ₀ _).hom,
    ← cancel_epi (singleObjCyclesSelfIso (ComplexShape.up ℕ) _ _).inv]

Premises used: HomologicalComplex.singleObjHomologySelfIso, HomologicalComplex.singleObjCyclesSelfIso, Nat, CochainComplex.isoHomologyπ₀, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, ComplexShape.up