-- Lean 4 proof step from Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : TopCat
F : Sheaf.{w, v_1, u_1} C X
U V : Opens (↑X : Type w)
s_1 :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
ι : ULift.{w, 0} WalkingPair → Opens (↑X : Type w) :=
  fun (x : ULift.{w, 0} WalkingPair) ↦
    match (motive := ULift.{w, 0} WalkingPair → Opens (↑X : Type w)) x with
    | { down := j } => WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j U V
hι : U ⊔ V = iSup ι
s :
  PullbackCone (X := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op U))
    (Y := F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj (op V))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
    (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
      (Quiver.Hom.op (homOfLE ⋯)))
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a : ULift.{w, 0} WalkingPair
⊢ Eq (α :=
    s.pt ⟶
      Functor.obj
        ({
            obj := fun (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
              op (Functor.obj (Pairwise.diagram ι) (unop X_1)),
            map := fun {X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ} (f : X_1 ⟶ Y) ↦
              Quiver.Hom.op (CategoryTheory.Functor.map (Pairwise.diagram ι) f.unop),
            map_id := ⋯, map_comp := ⋯ } ⋙
          F.presheaf)
        (op (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))
    (m ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯) ≫
            CategoryStruct.comp (Y := op (ι { down := WalkingPair.left }))
              (Quiver.Hom.op (homOfLE ⋯) :
                op
                    (Functor.obj
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)))
                        (Cocone.pt (Pairwise.cocone ι)))
                      (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)) ⟶
                  op (ι { down := WalkingPair.left }))
              (Quiver.Hom.op (homOfLE ⋯) :
                op (ι { down := WalkingPair.left : ULift.{w, 0} WalkingPair }) ⟶
                  op
                    (Functor.obj (Pairwise.diagram ι)
                      (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))) :
      s.pt ⟶
        Functor.obj
          ({
              obj := fun (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
                op (Functor.obj (Pairwise.diagram ι) (unop X_1)),
              map := fun {X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ} (f : X_1 ⟶ Y) ↦
                Quiver.Hom.op (CategoryTheory.Functor.map (Pairwise.diagram ι) f.unop),
              map_id := ⋯, map_comp := ⋯ } ⋙
            F.presheaf)
          (op (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))
    (F.interUnionPullbackConeLift U V s ≫
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (eqToHom ⋯) ≫
            CategoryStruct.comp (Y := op (ι { down := WalkingPair.left }))
              (Quiver.Hom.op (homOfLE ⋯) :
                op
                    (Functor.obj
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)))
                        (Cocone.pt (Pairwise.cocone ι)))
                      (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)) ⟶
                  op (ι { down := WalkingPair.left }))
              (Quiver.Hom.op (homOfLE ⋯) :
                op (ι { down := WalkingPair.left : ULift.{w, 0} WalkingPair }) ⟶
                  op
                    (Functor.obj (Pairwise.diagram ι)
                      (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))) :
      s.pt ⟶
        Functor.obj
          ({
              obj := fun (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
                op (Functor.obj (Pairwise.diagram ι) (unop X_1)),
              map := fun {X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ} (f : X_1 ⟶ Y) ↦
                Quiver.Hom.op (CategoryTheory.Functor.map (Pairwise.diagram ι) f.unop),
              map_id := ⋯, map_comp := ⋯ } ⋙
            F.presheaf)
          (op (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))
have property : Eq (α :=
  s.pt ⟶
    Functor.obj
      ({
          obj := fun (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
            op (Functor.obj (Pairwise.diagram ι) (unop X_1)),
          map := fun {X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ} (f : X_1 ⟶ Y) ↦
            Quiver.Hom.op (CategoryTheory.Functor.map (Pairwise.diagram ι) f.unop),
          map_id := sorry, map_comp := sorry } ⋙
        F.presheaf)
      (op (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))
  (CategoryStruct.comp (Y :=
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
        (op (ι { down := WalkingPair.left })))
      ((m ≫
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
              (Quiver.Hom.op (eqToHom sorry))) ≫
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
            (Quiver.Hom.op (homOfLE sorry)) :
        s.pt ⟶
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
            (op (ι { down := WalkingPair.left })))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE sorry)) :
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
            (op (ι { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
            (op
              (Functor.obj (Pairwise.diagram ι)
                (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))) :
    s.pt ⟶
      Functor.obj
        ({
            obj := fun (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
              op (Functor.obj (Pairwise.diagram ι) (unop X_1)),
            map := fun {X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ} (f : X_1 ⟶ Y) ↦
              Quiver.Hom.op (CategoryTheory.Functor.map (Pairwise.diagram ι) f.unop),
            map_id := sorry, map_comp := sorry } ⋙
          F.presheaf)
        (op (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))
  (CategoryStruct.comp (Y :=
      F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
        (op (ι { down := WalkingPair.left })))
      ((F.interUnionPullbackConeLift U V s ≫
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
              (Quiver.Hom.op (eqToHom sorry))) ≫
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
            (Quiver.Hom.op (homOfLE sorry)) :
        s.pt ⟶
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
            (op (ι { down := WalkingPair.left })))
      (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
          (Quiver.Hom.op (homOfLE sorry)) :
        F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
            (op (ι { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
          F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).obj
            (op
              (Functor.obj (Pairwise.diagram ι)
                (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))) :
    s.pt ⟶
      Functor.obj
        ({
            obj := fun (X_1 : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
              op (Functor.obj (Pairwise.diagram ι) (unop X_1)),
            map := fun {X_1 Y : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ} (f : X_1 ⟶ Y) ↦
              Quiver.Hom.op (CategoryTheory.Functor.map (Pairwise.diagram ι) f.unop),
            map_id := sorry, map_comp := sorry } ⋙
          F.presheaf)
        (op (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair } a)))
Tactic: simp_rw [F.1.map_comp, ← Category.assoc]