∀ {J : Type u_4} {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type u_1} {f : J → C} (c : CategoryTheory.Limits.Bicone f)
  (g : K ≃ J) (j : CategoryTheory.Discrete K),
  (c.whisker g).toCone.π.app j =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (c.whisker g).toCone.pt).hom
      (((CategoryTheory.Limits.Cones.postcompose (CategoryTheory.Discrete.functorComp f ⇑g).inv).obj
              (CategoryTheory.Limits.Cone.whisker (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑g))
                c.toCone)).π.app
        j)