-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
P : ProjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α := (F.leftDerived 0).obj X ⟶ F.obj X)
    (NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
          (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
            (F.mapHomologicalComplex (ComplexShape.down ℕ))
            (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X))) ≫
        HomologicalComplex.homologyι
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ))
              (Quotient.as (r := homotopic C (ComplexShape.down ℕ)) (Functor.obj (projectiveResolutions C) X)))
            0 ≫
          fromLeftDerivedZero' (projectiveResolution X) F :
      (F.leftDerived 0).obj X ⟶ F.obj X)
    ((Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) 0)
            (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F)) ≫
          NatTrans.app (Iso.hom (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) 0))
            (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex)) ≫
        HomologicalComplex.homologyι (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ≫
          P.fromLeftDerivedZero' F :
      (F.leftDerived 0).obj X ⟶ F.obj X)
have h₁ : Eq (α :=
  HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
  (CategoryStruct.comp (Y :=
      HomologicalComplex.opcycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
          (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
        0)
      (HomologicalComplex.opcyclesMap
          (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) (lift (𝟙 X) P (projectiveResolution X))) 0 :
        HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶
          HomologicalComplex.opcycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
            0)
      (fromLeftDerivedZero' (projectiveResolution X) F :
        HomologicalComplex.opcycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.down ℕ))
              (F.mapHomologicalComplex (ComplexShape.down ℕ)) (complex (projectiveResolution X)))
            0 ⟶
          F.obj X) :
    HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
  (P.fromLeftDerivedZero' F ≫ F.map (𝟙 X) :
    HomologicalComplex.opcycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) P.complex) 0 ⟶ F.obj X)
Tactic: have h₁ := ProjectiveResolution.fromLeftDerivedZero'_naturality
    (𝟙 X) P (projectiveResolution X) (lift (𝟙 X) _ _) (by simp) F