-- Module: Mathlib.Topology.Sheaves.Alexandrov
Goal:
X_1 : Type v
inst : TopologicalSpace X_1
inst_1 : Preorder X_1
inst_2 : Topology.IsUpperSet X_1
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F_1 : X_1 ⥤ C
X : TopCat
inst_5 : Preorder (↑X : Type v)
inst_6 : Topology.IsUpperSet.{v} (↑X : Type v)
F : CategoryTheory.Functor.{v, v, v, u} (↑X : Type v) C
α : Type v
Us : α → Opens (↑X : Type v)
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
V : Opens (↑X : Type v)
i : α
hV : V ≤ Us i
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op V)) left ⟶ obj (principals (↑X : Type v)) x
e : principalOpen x ≤ V
VV : OpensLeCover Us := ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯
xx : OpensLeCover Us :=
  ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) (principalOpen x) ⋯
ee : xx ⟶ VV := ObjectProperty.homMk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) e.hom
⊢ Eq (α :=
    Cone.pt.{v, v, v, u} (J :=
        StructuredArrow
          (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)) (Opposite.op xx))
          (principals (↑X : Type v)))
        (F :=
        StructuredArrow.proj
            (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)) (Opposite.op xx))
            (principals (↑X : Type v)) ⋙
          F)
        {
          pt :=
            limit (J :=
              StructuredArrow
                (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                  (Opposite.op VV))
                (principals (↑X : Type v)))
              (StructuredArrow.proj
                  (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                    (Opposite.op VV))
                  (principals (↑X : Type v)) ⋙
                F),
          π :=
            {
              app :=
                fun
                  (g :
                    StructuredArrow
                      (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                        (Opposite.op xx))
                      (principals (↑X : Type v))) ↦
                limit.π
                  (StructuredArrow.proj
                      (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                        (Opposite.op VV))
                      (principals (↑X : Type v)) ⋙
                    F)
                  (obj
                    (StructuredArrow.map
                      (CategoryTheory.Functor.map
                        (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)) ee.op))
                    g),
              naturality := ⋯ :
              NatTrans (C :=
                StructuredArrow
                  (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                    (Opposite.op xx))
                  (principals (↑X : Type v)))
                (obj
                  (Functor.const
                    (StructuredArrow
                      (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                        (Opposite.op xx))
                      (principals (↑X : Type v))))
                  (limit (J :=
                    StructuredArrow
                      (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                        (Opposite.op VV))
                      (principals (↑X : Type v)))
                    (StructuredArrow.proj
                        (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                          (Opposite.op VV))
                        (principals (↑X : Type v)) ⋙
                      F)))
                (StructuredArrow.proj
                    (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                      (Opposite.op xx))
                    (principals (↑X : Type v)) ⋙
                  F) } :
          Cone (J :=
            StructuredArrow
              (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)) (Opposite.op xx))
              (principals (↑X : Type v)))
            (StructuredArrow.proj
                (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                  (Opposite.op xx))
                (principals (↑X : Type v)) ⋙
              F) } ⟶
      obj (C :=
        StructuredArrow
          (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)) (Opposite.op xx))
          (principals (↑X : Type v)))
        (StructuredArrow.proj
            (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)) (Opposite.op xx))
            (principals (↑X : Type v)) ⋙
          F)
        { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) })
    (NatTrans.app
      (Cone.π
        {
          pt :=
            limit (J :=
              StructuredArrow
                (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                  (Opposite.op VV))
                (principals (↑X : Type v)))
              (StructuredArrow.proj
                  (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                    (Opposite.op VV))
                  (principals (↑X : Type v)) ⋙
                F),
          π :=
            {
              app :=
                fun
                  (g :
                    StructuredArrow
                      (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                        (Opposite.op xx))
                      (principals (↑X : Type v))) ↦
                limit.π
                  (StructuredArrow.proj
                      (obj (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i))
                        (Opposite.op VV))
                      (principals (↑X : Type v)) ⋙
                    F)
                  (obj
                    (StructuredArrow.map
                      (CategoryTheory.Functor.map
                        (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)) ee.op))
                    g),
              naturality := ⋯ } })
      { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) })
    (limit.π (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
      { left := left, right := x, hom := f })

Tactic:
aesop