∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Preorder X] [inst_2 : Topology.IsUpperSet X] {C : Type u_2}
  [inst_3 : CategoryTheory.Category.{u_1, u_2} C] [inst_4 : CategoryTheory.Limits.HasLimits C]
  {F : CategoryTheory.Functor X C} {α : Type u_1} (Us : α → TopologicalSpace.Opens X)
  (S :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.ObjectProperty.ι fun V => ∃ i, V ≤ Us i).op.comp (Alexandrov.principalsKanExtension F)))
  ⦃X_1 Y : CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (Alexandrov.principals X)⦄ (f : X_1 ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.const
                (CategoryTheory.StructuredArrow (Opposite.op (iSup Us)) (Alexandrov.principals X))).obj
            S.pt).map
        f)
      (CategoryTheory.CategoryStruct.comp (S.π.app ((Alexandrov.projSup Us).obj Y))
        (CategoryTheory.Limits.limit.π ((Alexandrov.generator (Alexandrov.principalOpen Y.right)).comp F)
          { left := { as := PUnit.unit }, right := Y.right,
            hom :=
              CategoryTheory.CategoryStruct.id
                ((CategoryTheory.Functor.fromPUnit (Opposite.op (Alexandrov.principalOpen Y.right))).obj
                  { as := PUnit.unit }) })) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (S.π.app ((Alexandrov.projSup Us).obj X_1))
        (CategoryTheory.Limits.limit.π ((Alexandrov.generator (Alexandrov.principalOpen X_1.right)).comp F)
          { left := { as := PUnit.unit }, right := X_1.right,
            hom :=
              CategoryTheory.CategoryStruct.id
                ((CategoryTheory.Functor.fromPUnit (Opposite.op (Alexandrov.principalOpen X_1.right))).obj
                  { as := PUnit.unit }) }))
      (((Alexandrov.generator (iSup Us)).comp F).map f)