Mathlib.CategoryTheory.Sites.EffectiveEpimorphic._auxLemma.1

theorem Mathlib.CategoryTheory.Sites.EffectiveEpimorphic._auxLemma.1 : ∀ {obj : Type u} [self : CategoryTheory.Category.{v, u} obj] {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h

The theorem `Mathlib.CategoryTheory.Sites.EffectiveEpimorphic._auxLemma.1` states that for any objects `W`, `X`, `Y`, and `Z` in a category, and any morphisms `f` from `W` to `X`, `g` from `X` to `Y`, and `h` from `Y` to `Z`, the composition of `f` with the composition of `g` and `h` is equal to the composition of the composition of `f` and `g` with `h`. In the language of category theory, this is asserting the associativity of morphism composition, i.e., the equation `(f ≫ (g ≫ h)) = ((f ≫ g) ≫ h)`.

More concisely: The theorem asserts the associativity of morphism composition in a category, that is, `(f ≫ g) ≫ h = f ≫ (g ≫ h)` for any morphisms `f: W → X`, `g: X → Y`, and `h: Y → Z`.