∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{u_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] {F : CategoryTheory.Functor C D} {Y : D} {D' : Type u_6}
  [inst_2 : CategoryTheory.Category.{u_5, u_6} D'] (G : CategoryTheory.Functor D D') [inst_3 : G.IsEquivalence]
  (j : CategoryTheory.CostructuredArrow F Y),
  CategoryTheory.CategoryStruct.comp
      ((G.mapCocone
              ((CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D) F.rightUnitor.inv).coconeAt
                Y)).ι.app
        j)
      (CategoryTheory.Iso.refl
          (G.mapCocone
              ((CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D) F.rightUnitor.inv).coconeAt
                Y)).pt).hom =
    (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.CostructuredArrow.post F G Y).asEquivalence.functor
            ((CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D')
                  (F.comp G).rightUnitor.inv).coconeAt
              (G.obj Y))).ι.app
      j