∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] {X Y : C} (f : X ⟶ Y)
  (hf : W f) (g : X ⟶ Z) {Z_1 : C} (h : ∐ CategoryTheory.OrthogonalReflection.D₁.obj₂ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.ιRight f hf g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.ιLeft f hf g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.OrthogonalReflection.D₁.t W Z) h)