Mathlib.CategoryTheory.Triangulated.TriangleShift._auxLemma.1

theorem Mathlib.CategoryTheory.Triangulated.TriangleShift._auxLemma.1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (self : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (self.map f) (self.map g) = self.map (CategoryTheory.CategoryStruct.comp f g)

This theorem states that for any two categories `C` and `D`, given a functor `self` from `C` to `D` and three objects `X`, `Y`, and `Z` in `C` with morphisms `f` from `X` to `Y` and `g` from `Y` to `Z`, the composition of the images of `f` and `g` under `self` is equal to the image under `self` of the composition of `f` and `g` in `C`. In other words, the functor `self` preserves the composition of morphisms, a property known as functoriality.

More concisely: For any functors `self: C → D` between categories `C` and `D`, and objects `X, Y, Z` in `C` with morphisms `f: X → Y` and `g: Y → Z`, the equality `self(f ∘ g) = self(f) ∘ self(g)` holds.