∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct (f ∘ ⇑ε)] (b : β) {Z : C}
  (h : ∐ f ∘ ⇑ε ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f (ε b))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.reindex ε f).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (f ∘ ⇑ε) b) h