-- 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)
m :
  S.pt ⟶
    Cone.pt (F :=
      Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
      (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)
hm_1 :
  ∀
    (j :
      (ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
          ∃ (i : α), V ≤ Us i)ᵒᵖ),
    m ≫ NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op)) j = S.π.app j
left : Discrete PUnit.{1}
x : (↑X : Type v)
f : obj (fromPUnit (Opposite.op (iSup Us))) left ⟶ obj (principals (↑X : Type v)) x
hm :
  Eq (α :=
    S.pt ⟶
      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)
            (principalOpen x) ⋯)))
    (m ≫
      NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op))
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
            (principalOpen x) ⋯)))
    (S.π.app
      (Opposite.op
        (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) (principalOpen x)
          ⋯)))
w :
  Eq (α :=
    Cone.pt (F :=
        Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
        (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op) ⟶
      F.obj
        (obj (generator (iSup Us))
          { left := left, right := x, hom := f :
            Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))
    (CategoryStruct.comp (Y :=
        limit (J :=
          StructuredArrow (D := (Opens (↑X : Type v))ᵒᵖ)
            (Opposite.op
              (obj (C :=
                ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
                  ∃ (i : α), V ≤ Us i)
                (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                  (principalOpen
                    (StructuredArrow.right
                      { left := left, right := x, hom := f :
                        Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))
                  ⋯)))
            (principals (↑X : Type v)))
          (StructuredArrow.proj
              (Opposite.op
                (obj (C :=
                  ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
                    ∃ (i : α), V ≤ Us i)
                  (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                  (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                    (principalOpen
                      (StructuredArrow.right
                        { left := left, right := x, hom := f :
                          Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))
                    ⋯)))
              (principals (↑X : Type v)) ⋙
            F))
        (NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op))
          (Opposite.op
            (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
              (principalOpen x) ⋯)))
        (limit.π
          (generator
              (principalOpen
                (StructuredArrow.right
                  { left := left, right := x, hom := f :
                    Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) })) ⋙
            F)
          { left := { as := PUnit.unit },
            right :=
              StructuredArrow.right
                { left := left, right := x, hom := f :
                  Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) },
            hom :=
              𝟙
                (Opposite.op
                  (principalOpen
                    (StructuredArrow.right
                      { left := left, right := x, hom := f :
                        Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))) }) :
      Cone.pt (F :=
          Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
          (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op) ⟶
        F.obj
          (obj (generator (iSup Us))
            { left := left, right := x, hom := f :
              Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))
    (limit.π (generator (iSup Us) ⋙ F) { left := left, right := x, hom := f } :
      limit (J := StructuredArrow (Opposite.op (iSup Us)) (principals (↑X : Type v))) (generator (iSup Us) ⋙ F) ⟶
        obj (generator (iSup Us) ⋙ F)
          { left := left, right := x, hom := f : Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) })
⊢ m ≫
      CategoryStruct.comp (Y :=
        limit (J :=
          StructuredArrow (D := (Opens (↑X : Type v))ᵒᵖ)
            (Opposite.op
              (obj (C :=
                ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
                  ∃ (i : α), V ≤ Us i)
                (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                  (principalOpen
                    (StructuredArrow.right
                      { left := left, right := x, hom := f :
                        Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))
                  ⋯)))
            (principals (↑X : Type v)))
          (StructuredArrow.proj
              (Opposite.op
                (obj (C :=
                  ObjectProperty.FullSubcategory (C := Opens (↑X : Type v)) fun (V : Opens (↑X : Type v)) ↦
                    ∃ (i : α), V ≤ Us i)
                  (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                  (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
                    (principalOpen
                      (StructuredArrow.right
                        { left := left, right := x, hom := f :
                          Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))
                    ⋯)))
              (principals (↑X : Type v)) ⋙
            F))
        (NatTrans.app (Cone.π (mapCone (principalsKanExtension F) (opensLeCoverCocone Us).op))
          (Opposite.op
            (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
              (principalOpen x) ⋯)))
        (limit.π
          (generator
              (principalOpen
                (StructuredArrow.right
                  { left := left, right := x, hom := f :
                    Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) })) ⋙
            F)
          { left := { as := PUnit.unit },
            right :=
              StructuredArrow.right
                { left := left, right := x, hom := f :
                  Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) },
            hom :=
              𝟙
                (Opposite.op
                  (principalOpen
                    (StructuredArrow.right
                      { left := left, right := x, hom := f :
                        Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }))) }) =
    m ≫
      limit.π (generator (iSup Us) ⋙ F)
        { left := left, right := x, hom := f : Comma (fromPUnit (Opposite.op (iSup Us))) (principals (↑X : Type v)) }

Tactic:
congr