C : Type u
inst✝¹² : Category C
D : Type u_2
inst✝¹¹ : Category D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ 𝟙
      (projectiveResolutions C ⋙
        Functor.mapHomotopyCategory F (ComplexShape.down ℕ) ⋙
          HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (Functor.leftDerived F n)
C : Type u
inst✝¹² : Category C
D : Type u_2
inst✝¹¹ : Category D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ leftDerived (𝟙 F) n = 𝟙 (Functor.leftDerived F n)
simp [NatTrans.leftDerived]
no goals
C : Type u
inst✝¹² : Category C
D : Type u_2
inst✝¹¹ : Category D
inst✝¹⁰ : Preadditive C
inst✝⁹ : HasZeroObject C
inst✝⁸ : HasEqualizers C
inst✝⁷ : HasImages C
inst✝⁶ : HasProjectiveResolutions C
inst✝⁵ : Preadditive D
inst✝⁴ : HasEqualizers D
inst✝³ : HasCokernels D
inst✝² : HasImages D
inst✝¹ : HasImageMaps D
F : C ⥤ D
inst✝ : Functor.Additive F
n : ℕ
⊢ 𝟙
      (projectiveResolutions C ⋙
        Functor.mapHomotopyCategory F (ComplexShape.down ℕ) ⋙
          HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n) =
    𝟙 (Functor.leftDerived F n)
rfl