-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.RightDerived (goal)
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 : HasInjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X : C
I : InjectiveResolution.{v, u} X
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α := F.obj X ⟶ (F.rightDerived 0).obj X) (NatTrans.app F.toRightDerivedZero X)
    (CategoryStruct.comp (Y :=
      HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
      (I.toRightDerivedZero' F :
        F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
      (Iso.hom (CochainComplex.isoHomologyπ₀ (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex)) ≫
          Iso.inv (I.isoRightDerivedObj F 0) :
        HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0 ⟶
          (F.rightDerived 0).obj X))
have dsimp : Eq (α := F.obj X ⟶ (F.rightDerived 0).obj X)
  (CategoryStruct.comp (Y :=
      HomologicalComplex.cycles
        (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
          (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
        0)
      (toRightDerivedZero' (injectiveResolution X) F :
        F.obj X ⟶
          HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
            0)
      (HomologicalComplex.homologyπ
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
            0 ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X))) :
        HomologicalComplex.cycles
            (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
              (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
            0 ⟶
          (F.rightDerived 0).obj X) :
    F.obj X ⟶ (F.rightDerived 0).obj X)
  (CategoryStruct.comp (Y :=
      HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
      (I.toRightDerivedZero' F :
        F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
      (HomologicalComplex.homologyπ (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0 ≫
          NatTrans.app (Iso.inv (HomotopyCategory.homologyFunctorFactors D (ComplexShape.up ℕ) 0))
              (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) ≫
            Functor.map (HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) 0)
              (Iso.inv (I.isoRightDerivedToHomotopyCategoryObj F)) :
        HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0 ⟶
          (F.rightDerived 0).obj X) :
    F.obj X ⟶ (F.rightDerived 0).obj X)
Tactic: dsimp [Functor.toRightDerivedZero, isoRightDerivedObj]