-- Module: Mathlib.CategoryTheory.Abelian.RightDerived
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
h₁ :
  Eq (α :=
    F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (F.map (𝟙 X) ≫ I.toRightDerivedZero' F :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
    (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.cyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) (desc (𝟙 X) I (injectiveResolution X))) 0 :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0) :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)
⊢ Eq (α :=
    F.obj X ⟶ 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)
    (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.cyclesMap
            (Functor.map (F.mapHomologicalComplex (ComplexShape.up ℕ)) (desc (𝟙 X) I (injectiveResolution X))) 0 :
          HomologicalComplex.cycles
              (Functor.obj (C := HomologicalComplex.{v, u, 0} C (ComplexShape.up ℕ))
                (F.mapHomologicalComplex (ComplexShape.up ℕ)) (cocomplex (injectiveResolution X)))
              0 ⟶
            HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0) :
      F.obj X ⟶ HomologicalComplex.cycles (Functor.obj (F.mapHomologicalComplex (ComplexShape.up ℕ)) I.cocomplex) 0)

Tactic:
simp only [Functor.map_id, id_comp] at h₁

Premises used: CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp