-- Lean 4 proof step from Mathlib.Topology.Sheaves.Alexandrov (goal)
Goal:
X : Type v
inst : TopologicalSpace X
inst_1 : Preorder X
inst_2 : Topology.IsUpperSet X
C : Type u
inst_3 : Category.{v, u} C
inst_4 : HasLimits.{v, u} C
F : X ⥤ C
α : Type v
Us : α → Opens X
S :
  Cone (J :=
    (ObjectProperty.FullSubcategory (C := Opens (↑(of X) : Type v)) fun (V : Opens (↑(of X) : Type v)) ↦
        ∃ (i : α), V ≤ Us i)ᵒᵖ)
    (Functor.op (ObjectProperty.ι fun (V : Opens (↑(of X) : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙ principalsKanExtension F)
x y : StructuredArrow (Opposite.op (iSup Us)) (principals X)
e : x ⟶ y
⊢ Eq (α := S.pt ⟶ F.obj (obj (generator (iSup Us)) y))
    (CategoryStruct.comp (Y :=
        limit (J :=
          StructuredArrow
            (Opposite.op
              (obj (ObjectProperty.ι fun (V : Opens X) ↦ ∃ (i : α), V ≤ Us i) (Opposite.unop (obj (projSup Us) y))))
            (principals X))
          (StructuredArrow.proj
              (Opposite.op
                (obj (ObjectProperty.ι fun (V : Opens X) ↦ ∃ (i : α), V ≤ Us i) (Opposite.unop (obj (projSup Us) y))))
              (principals X) ⋙
            F))
        (S.π.app (obj (projSup Us) y))
        (limit.π (generator (principalOpen y.right) ⋙ F)
          { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) }) :
      S.pt ⟶ F.obj (obj (generator (iSup Us)) y))
    (CategoryStruct.comp (Y :=
        limit (J :=
          StructuredArrow
            (Opposite.op
              (obj (ObjectProperty.ι fun (V : Opens X) ↦ ∃ (i : α), V ≤ Us i) (Opposite.unop (obj (projSup Us) x))))
            (principals X))
          (StructuredArrow.proj
              (Opposite.op
                (obj (ObjectProperty.ι fun (V : Opens X) ↦ ∃ (i : α), V ≤ Us i) (Opposite.unop (obj (projSup Us) x))))
              (principals X) ⋙
            F))
        (S.π.app (obj (projSup Us) x))
        (CategoryStruct.comp (Y := F.obj (obj (generator (iSup Us)) x))
          (limit.π (generator (principalOpen x.right) ⋙ F)
              { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) } :
            limit (J := StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X))
                (generator (principalOpen x.right) ⋙ F) ⟶
              obj (C := StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X))
                (generator (principalOpen x.right) ⋙ F)
                { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) })
          (F.map (CategoryTheory.Functor.map (generator (iSup Us)) e))) :
      S.pt ⟶ F.obj (obj (generator (iSup Us)) y))
have rw : Eq (α := S.pt ⟶ F.obj (obj (generator (iSup Us)) y))
  (CategoryStruct.comp (Y :=
      obj
        (Functor.op (ObjectProperty.ι fun (V : Opens (↑(of X) : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙
          principalsKanExtension F)
        (obj (projSup Us) x))
      (S.π.app (obj (projSup Us) x))
      (CategoryTheory.Functor.map
          (Functor.op (ObjectProperty.ι fun (V : Opens (↑(of X) : Type v)) ↦ ∃ (i : α), V ≤ Us i) ⋙
            principalsKanExtension F)
          (CategoryTheory.Functor.map (projSup Us) e) ≫
        limit.π (generator (principalOpen y.right) ⋙ F)
          { left := { as := PUnit.unit }, right := y.right, hom := 𝟙 (Opposite.op (principalOpen y.right)) }) :
    S.pt ⟶ F.obj (obj (generator (iSup Us)) y))
  (CategoryStruct.comp (Y :=
      limit (J :=
        StructuredArrow
          (Opposite.op
            (obj (ObjectProperty.ι fun (V : Opens X) ↦ ∃ (i : α), V ≤ Us i) (Opposite.unop (obj (projSup Us) x))))
          (principals X))
        (StructuredArrow.proj
            (Opposite.op
              (obj (ObjectProperty.ι fun (V : Opens X) ↦ ∃ (i : α), V ≤ Us i) (Opposite.unop (obj (projSup Us) x))))
            (principals X) ⋙
          F))
      (S.π.app (obj (projSup Us) x))
      (CategoryStruct.comp (Y := F.obj (obj (generator (iSup Us)) x))
        (limit.π (generator (principalOpen x.right) ⋙ F)
            { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) } :
          limit (J := StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X))
              (generator (principalOpen x.right) ⋙ F) ⟶
            obj (C := StructuredArrow (D := (Opens X)ᵒᵖ) (Opposite.op (principalOpen x.right)) (principals X))
              (generator (principalOpen x.right) ⋙ F)
              { left := { as := PUnit.unit }, right := x.right, hom := 𝟙 (Opposite.op (principalOpen x.right)) })
        (F.map (CategoryTheory.Functor.map (generator (iSup Us)) e))) :
    S.pt ⟶ F.obj (obj (generator (iSup Us)) y))
Tactic: rw [← S.w ((projSup Us).map e), Category.assoc]