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 G H : C ⥤ D
inst✝² : Functor.Additive F
inst✝¹ : Functor.Additive G
inst✝ : Functor.Additive H
α : F ⟶ G
β : G ⟶ H
n : ℕ
⊢ leftDerived (α ≫ β) n = leftDerived α n ≫ leftDerived β n
simp [NatTrans.leftDerived]