Composition of degree-zero shifted morphisms in a localization

Two composition lemmas for SmallShiftedHom that Mathlib's SmallShiftedHom.mk₀ API lacks at the pin: composing two degree-zero shifted morphisms, and composing a shifted morphism with a degree-zero one. Both are stated for an arbitrary morphism property compatible with the shift; their use for the injective-resolution presentation of Ext is in Algebra/Homology/DerivedCategory/Ext/InjectiveResolutionNaturality.lean.

theorem CategoryTheory.Localization.SmallShiftedHom.mk₀_comp_mk₀' {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {M : Type u_1} [AddMonoid M] [HasShift C M] [W.IsCompatibleWithShift M] {X Y Z : C} [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Z] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) (g : Y ⟶ Z) : (mk₀ W m₀ hm₀ f).comp (mk₀ W m₀ hm₀ g) ⋯ = mk₀ W m₀ hm₀ (CategoryStruct.comp f g)

Composing two degree-zero shifted morphisms is the degree-zero shifted composition.

theorem CategoryTheory.Localization.SmallShiftedHom.mk_comp_mk₀ {C : Type u} [Category.{v, u} C] {W : MorphismProperty C} {M : Type u_1} [AddMonoid M] [HasShift C M] [W.IsCompatibleWithShift M] {X Y Z : C} [HasSmallLocalizedShiftedHom W M X Y] [HasSmallLocalizedShiftedHom W M Y Z] [HasSmallLocalizedShiftedHom W M X Z] [HasSmallLocalizedShiftedHom W M Z Z] {m : M} (f : ShiftedHom X Y m) (m₀ : M) (hm₀ : m₀ = 0) (g : Y ⟶ Z) : (mk W f).comp (mk₀ W m₀ hm₀ g) ⋯ = mk W (CategoryStruct.comp f ((shiftFunctor C m).map g))

Composing a shifted morphism with a degree-zero one is the shifted composition.