CategoryTheory.eq_whisker'

theorem CategoryTheory.eq_whisker' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : C} {f g : X ⟶ Y}, f = g → ∀ {Z : C} (h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h

The theorem `CategoryTheory.eq_whisker'` states that in any category `C`, if we have two morphisms `f` and `g` from object `X` to `Y` that are equal, then for any object `Z` in `C` and any morphism `h` from `Y` to `Z`, the composition of `f` and `h` is equal to the composition of `g` and `h`. In other words, if `f` equals `g`, then composing `f` or `g` with `h` (in that order) gives the same result. This theorem is a variant of `eq_whisker` with a different argument order designed to be more convenient for use in tactics.

More concisely: In any category, if two morphisms from an object to another are equal, then their composition with any morphism from the second object to a third is equal.