C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ 𝟙
      (injectiveResolutions C ⋙
        Functor.mapHomotopyCategory F (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (Functor.rightDerived F n)
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ rightDerived (𝟙 F) n = 𝟙 (Functor.rightDerived F n)
simp [NatTrans.rightDerived]
no goals
C : Type u
inst✝⁵ : Category C
D : Type u_2
inst✝⁴ : Category D
inst✝³ : Abelian C
inst✝² : HasInjectiveResolutions C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ 𝟙
      (injectiveResolutions C ⋙
        Functor.mapHomotopyCategory F (ComplexShape.up ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.up ℕ) n) =
    𝟙 (Functor.rightDerived F n)
rfl