-- 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
w :
  ∀ (left : Discrete PUnit.{1}) (x : (↑X : Type v))
    (f : obj (fromPUnit (Opposite.op V)) left ⟶ obj (principals (↑X : Type v)) x),
    Eq (α :=
      S.pt ⟶
        obj (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
          { left := left, right := x, hom := f : Comma (fromPUnit (Opposite.op V)) (principals (↑X : Type v)) })
      (CategoryStruct.comp (Y :=
        limit (J := StructuredArrow (Opposite.op V) (principals (↑X : Type v)))
          (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F))
        (CategoryStruct.comp (Y :=
          limit (J := StructuredArrow (Opposite.op (iSup Us)) (principals (↑X : Type v)))
            (StructuredArrow.proj (Opposite.op (iSup Us)) (principals (↑X : Type v)) ⋙ F))
          (limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S))
          (limit.lift (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
            {
              pt :=
                limit (J := StructuredArrow (Opposite.op (iSup Us)) (principals (↑X : Type v)))
                  (StructuredArrow.proj (Opposite.op (iSup Us)) (principals (↑X : Type v)) ⋙ F),
              π :=
                {
                  app := fun (g : StructuredArrow (Opposite.op V) (principals (↑X : Type v))) ↦
                    limit.π (StructuredArrow.proj (Opposite.op (iSup Us)) (principals (↑X : Type v)) ⋙ F)
                      (obj
                        (StructuredArrow.map
                          (CategoryStruct.comp (Y :=
                            Opposite.op
                              (Us
                                (OpensLeCover.index (U := Us)
                                  (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦
                                    ∃ (i : α), V ≤ Us i) V ⋯))))
                            (Quiver.Hom.op
                              (Opens.leSupr Us
                                (OpensLeCover.index (U := Us)
                                  (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦
                                    ∃ (i : α), V ≤ Us i) V ⋯))))
                            (Quiver.Hom.op
                              (OpensLeCover.homToIndex
                                (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦
                                  ∃ (i : α), V ≤ Us i) V ⋯)))))
                        g),
                  naturality := ⋯ } }))
        (limit.π (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
          { left := left, right := x, hom := f }))
      (CategoryStruct.comp (Y :=
        limit (J := StructuredArrow (Opposite.op V) (principals (↑X : Type v)))
          (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F))
        (S.π.app
            (Opposite.op
              (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯)) :
          obj (C :=
              (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
                  ∃ (i : α), V ≤ Us i)ᵒᵖ)
              (obj
                (Functor.const
                  (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
                      ∃ (i : α), V ≤ Us i)ᵒᵖ)
                S.pt)
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯)) ⟶
            obj (C :=
              (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)
              (Opposite.op
                (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯)))
        (limit.π (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
          { left := left, right := x, hom := f }))
⊢ Eq (α :=
    S.pt ⟶
      limit (J := StructuredArrow (Opposite.op V) (principals (↑X : Type v)))
        (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F))
    (CategoryStruct.comp (Y :=
        limit (J := StructuredArrow (Opposite.op (iSup Us)) (principals (↑X : Type v)))
          (StructuredArrow.proj (Opposite.op (iSup Us)) (principals (↑X : Type v)) ⋙ F))
        (limit.lift (generator (iSup Us) ⋙ F) (lowerCone Us S))
        (limit.lift (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
          {
            pt :=
              limit (J := StructuredArrow (Opposite.op (iSup Us)) (principals (↑X : Type v)))
                (StructuredArrow.proj (Opposite.op (iSup Us)) (principals (↑X : Type v)) ⋙ F),
            π :=
              {
                app := fun (g : StructuredArrow (Opposite.op V) (principals (↑X : Type v))) ↦
                  limit.π (StructuredArrow.proj (Opposite.op (iSup Us)) (principals (↑X : Type v)) ⋙ F)
                    (obj
                      (StructuredArrow.map
                        (CategoryStruct.comp (Y :=
                          Opposite.op
                            (Us
                              (OpensLeCover.index (U := Us)
                                (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦
                                  ∃ (i : α), V ≤ Us i) V ⋯))))
                          (Quiver.Hom.op
                            (Opens.leSupr Us
                              (OpensLeCover.index (U := Us)
                                (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦
                                  ∃ (i : α), V ≤ Us i) V ⋯))))
                          (Quiver.Hom.op
                            (OpensLeCover.homToIndex
                              (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦
                                ∃ (i : α), V ≤ Us i) V ⋯)))))
                      g),
                naturality := ⋯ } }) :
      S.pt ⟶
        limit (J := StructuredArrow (Opposite.op V) (principals (↑X : Type v)))
          (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F))
    (S.π.app
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯)) :
      obj (C :=
          (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
              ∃ (i : α), V ≤ Us i)ᵒᵖ)
          (obj
            (Functor.const
              (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
                  ∃ (i : α), V ≤ Us i)ᵒᵖ)
            S.pt)
          (Opposite.op
            (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯)) ⟶
        obj (C :=
          (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)
          (Opposite.op
            (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V ⋯)))

Tactic:
ext ⟨_, x, f⟩