Small congruence lemmas for categorical composition

theorem MagnitudeConjecture.precomp_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) {g h : Y ⟶ Z} (e : g = h) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h

Precomposition preserves equality of morphisms. Naming this generic operation prevents downstream elaboration from expanding a large concrete morphism family inside congrArg.

theorem MagnitudeConjecture.assoc_comp_congr {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : W ⟶ X) {g : X ⟶ Y} {h : Y ⟶ Z} {l : X ⟶ Z} (e : CategoryTheory.CategoryStruct.comp g h = l) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f l

An equality of a two-step composite remains true after one further precomposition, with reassociation performed generically.