∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C}
  (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [inst_1 : CategoryTheory.Limits.HasCoproduct f]
  [inst_2 : CategoryTheory.Limits.HasCoproduct g],
  (CategoryTheory.Limits.Sigma.whiskerEquiv e w).hom = CategoryTheory.Limits.Sigma.map' ⇑e fun j => (w j).inv