-- Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
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 :
  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 (j : ULift.{w, 0} WalkingPair) ↦
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ Opens (↑X : Type w)) j.down U V
hι : U ⊔ V = iSup ι
j : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)
g : j ⟶ Pairwise.single { down := WalkingPair.left }
refine_2 :
  ∀
    (g :
      Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair } ⟶
        Pairwise.single { down := WalkingPair.left }),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{w, v_1, w, u_1}
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.left })))
      (CategoryTheory.Functor.map
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) g.op ≫
        Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯))))
      ((Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))) ≫
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).map g.op)
refine_2₁ :
  ∀
    (g :
      Pairwise.single { down := WalkingPair.right : ULift.{w, 0} WalkingPair } ⟶
        Pairwise.single { down := WalkingPair.left }),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{w, v_1, w, u_1}
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := WalkingPair.right })))
      (CategoryTheory.Functor.map
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) g.op ≫
        Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op (Pairwise.single { down := WalkingPair.right : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯))))
      ((Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))) ≫
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).map g.op)
refine_2₂ :
  ∀ (down : WalkingPair)
    (g :
      Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair }
          { down := down : ULift.{w, 0} WalkingPair } ⟶
        Pairwise.single { down := WalkingPair.left }),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{w, v_1, w, u_1}
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj
          (op (Pairwise.pair { down := WalkingPair.left } { down := down })))
      (CategoryTheory.Functor.map
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) g.op ≫
        Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op
            (Pairwise.pair { down := WalkingPair.left : ULift.{w, 0} WalkingPair }
              { down := down : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯))))
      ((Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))) ≫
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).map g.op)
refine_2₃ :
  ∀ (down : WalkingPair)
    (g :
      Pairwise.pair { down := WalkingPair.right : ULift.{w, 0} WalkingPair }
          { down := down : ULift.{w, 0} WalkingPair } ⟶
        Pairwise.single { down := WalkingPair.left }),
    Eq.{v_1 + 1} (α :=
      Functor.obj.{w, v_1, w, u_1}
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj
          (op (Pairwise.pair { down := WalkingPair.right } { down := down })))
      (CategoryTheory.Functor.map
          (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) g.op ≫
        Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op
            (Pairwise.pair { down := WalkingPair.right : ULift.{w, 0} WalkingPair }
              { down := down : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯))))
      ((Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
          (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair }))
          fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
            unop
            (fun (a : ULift.{w, 0} WalkingPair) ↦
              ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single x)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
                a fun (down : WalkingPair) ↦
                WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                  Functor.obj.{w, v_1, w, u_1}
                      (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                      (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                    (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                  down s.fst s.snd)
            fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair x a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
                down
                (s.fst ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))
                (s.snd ≫
                  F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                    (Quiver.Hom.op (homOfLE ⋯)))) ≫
        (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).map g.op)
⊢ Eq.{v_1 + 1} (α :=
    Functor.obj.{w, v_1, w, u_1}
        (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
        (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair })) ⟶
      (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op j))
    (CategoryTheory.Functor.map
        (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) g.op ≫
      Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
        Functor.obj.{w, v_1, w, u_1}
            (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
          (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
        (op j) fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
        Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
          unop
          (fun (a : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.single x)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                down s.fst s.snd)
          fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
          ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                (op (Pairwise.pair x a_1)) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
            a fun (down : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
              down
              (s.fst ≫
                F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯)))
              (s.snd ≫
                F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯))))
    ((Opposite.casesOn (motive := fun (x : (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) ↦
        Functor.obj.{w, v_1, w, u_1}
            (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) x ⟶
          (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj x)
        (op (Pairwise.single { down := WalkingPair.left : ULift.{w, 0} WalkingPair }))
        fun (unop : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
        Pairwise.casesOn (motive := fun (x : CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair)) ↦
          Functor.obj.{w, v_1, w, u_1}
              (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt) (op x) ⟶
            (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op x))
          unop
          (fun (a : ULift.{w, 0} WalkingPair) ↦
            ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.single x)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single x)))
              a fun (down : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
                Functor.obj.{w, v_1, w, u_1}
                    (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                    (op (Pairwise.single { down := x : ULift.{w, 0} WalkingPair })) ⟶
                  (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.single { down := x })))
                down s.fst s.snd)
          fun (a a_1 : ULift.{w, 0} WalkingPair) ↦
          ULift.casesOn (motive := fun (x : ULift.{w, 0} WalkingPair) ↦
            Functor.obj.{w, v_1, w, u_1}
                (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                (op (Pairwise.pair x a_1)) ⟶
              (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair x a_1)))
            a fun (down : WalkingPair) ↦
            WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
              Functor.obj.{w, v_1, w, u_1}
                  (Functor.obj (Functor.const (CategoryTheory.Pairwise (ULift.{w, 0} WalkingPair))ᵒᵖ) s.pt)
                  (op (Pairwise.pair { down := x : ULift.{w, 0} WalkingPair } a_1)) ⟶
                (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).obj (op (Pairwise.pair { down := x } a_1)))
              down
              (s.fst ≫
                F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯)))
              (s.snd ≫
                F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type w))).map
                  (Quiver.Hom.op (homOfLE ⋯)))) ≫
      (Functor.op (Pairwise.diagram ι) ⋙ F.presheaf).map g.op)

Tactic:
rcases j with (⟨⟨_ | _⟩⟩ | ⟨⟨_ | _⟩, ⟨_⟩⟩)