-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
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 (α := S.pt ⟶ F.obj x)
    (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 x) ⋯)))
            (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 x) ⋯)))
              (principals (↑X : Type v)) ⋙
            F))
        (S.π.app
          (Opposite.op
            (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i)
              (principalOpen x) ⋯)))
        (limit.π (generator (principalOpen x) ⋙ F)
          { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) }) :
      S.pt ⟶ F.obj x)
    (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 }) :
      S.pt ⟶ F.obj x)
have w : Eq (α := S.pt ⟶ F.obj x)
  (S.π.app (Opposite.op VV) ≫
    CategoryTheory.Functor.map
        (Functor.op (ObjectProperty.ι fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
        ee.op ≫
      limit.π (generator (principalOpen x) ⋙ F)
        { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) :
          Comma (T := (Opens (↑X : Type v))ᵒᵖ) (fromPUnit (Opposite.op (principalOpen x))) (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))
    (S.π.app
        (Opposite.op
          (ObjectProperty.FullSubcategory.mk (P := fun (V : Opens (↑X : Type v)) ↦ ∃ (i : α), V ≤ Us i) V sorry)) :
      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 sorry)) ⟶
        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 sorry)))
    (limit.π (StructuredArrow.proj (Opposite.op V) (principals (↑X : Type v)) ⋙ F)
      { left := left, right := x, hom := f }))
Tactic: rw [← S.w ee.op, Category.assoc]