-- Module: Mathlib.Topology.Sheaves.CommRingCat
Goal:
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens (↑X : Type u)
e : W ≤ U ⊔ V
x :
  (↑(CommRingCat.of
        ↥(RingHom.eqLocus
            (RingHom.comp
              (CommRingCat.Hom.hom
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
                  (Quiver.Hom.op (homOfLE ⋯))))
              (RingHom.fst
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
                  Type u)
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op V)) :
                  Type u)))
            (RingHom.comp
              (CommRingCat.Hom.hom
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
                  (Quiver.Hom.op (homOfLE ⋯))))
              (RingHom.snd
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) :
                  Type u)
                (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op V)) :
                  Type u))))) :
    Type u)
y : (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) : Type u)
e₁ :
  Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op U)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op U)) : Type u)) → (↑(F.obj.obj (op (U ⊓ W))) : Type u))
        (↑x : (↑(F.obj.obj (op U)) : Type u) × (↑(F.obj.obj (op V)) : Type u)).1 :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op W)) : Type u)) → (↑(F.obj.obj (op (U ⊓ W))) : Type u))
        y :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W))) :
        Type u))
e₂ :
  Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op V)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op V)) : Type u)) → (↑(F.obj.obj (op (V ⊓ W))) : Type u))
        (↑x : (↑(F.obj.obj (op U)) : Type u) × (↑(F.obj.obj (op V)) : Type u)).2 :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op W)) : Type u)) → (↑(F.obj.obj (op (V ⊓ W))) : Type u))
        y :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W))) :
        Type u))
mpr : W ≤ U ⊓ W ⊔ V ⊓ W
mpr₁ :
  Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op W)) : Type u)) → (↑(F.obj.obj (op (U ⊓ W))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
                  (homOfLE e).op) :
              (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u)) → (↑(F.obj.obj (op W)) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (F.objSupIsoProdEqLocus U V).inv :
                  (a :
                      (↑(CommRingCat.of
                            ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                                    (RingHom.fst (↑(F.obj.obj (op U)) : Type u) (↑(F.obj.obj (op V)) : Type u))).eqLocus
                                ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                                  (RingHom.snd (↑(F.obj.obj (op U)) : Type u) (↑(F.obj.obj (op V)) : Type u))))) :
                        Type u)) →
                    (↑(F.obj.obj (op (U ⊔ V))) : Type u))
                x :
              (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
                    (op (U ⊔ V))) :
                Type u)) :
          (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) :
            Type u)) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op W)) : Type u)) → (↑(F.obj.obj (op (U ⊓ W))) : Type u))
        y :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊓ W))) :
        Type u))
mpr₂ :
  Eq (α :=
    (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op W)) : Type u)) → (↑(F.obj.obj (op (V ⊓ W))) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier)
                (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
                  (homOfLE e).op) :
              (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u)) → (↑(F.obj.obj (op W)) : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (F.objSupIsoProdEqLocus U V).inv :
                  (a :
                      (↑(CommRingCat.of
                            ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                                    (RingHom.fst (↑(F.obj.obj (op U)) : Type u) (↑(F.obj.obj (op V)) : Type u))).eqLocus
                                ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                                  (RingHom.snd (↑(F.obj.obj (op U)) : Type u) (↑(F.obj.obj (op V)) : Type u))))) :
                        Type u)) →
                    (↑(F.obj.obj (op (U ⊔ V))) : Type u))
                x :
              (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj
                    (op (U ⊔ V))) :
                Type u)) :
          (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) :
            Type u)) :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op W)) (Y :=
            F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W)))
            (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(F.obj.obj (op W)) : Type u)) → (↑(F.obj.obj (op (V ⊓ W))) : Type u))
        y :
      (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (V ⊓ W))) :
        Type u))
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)
          (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map (homOfLE e).op) :
        (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u)) → (↑(F.obj.obj (op W)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (F.objSupIsoProdEqLocus U V).inv :
            (a :
                (↑(CommRingCat.of
                      ↥(((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                              (RingHom.fst (↑(F.obj.obj (op U)) : Type u) (↑(F.obj.obj (op V)) : Type u))).eqLocus
                          ((CommRingCat.Hom.hom (F.obj.map (homOfLE ⋯).op)).comp
                            (RingHom.snd (↑(F.obj.obj (op U)) : Type u) (↑(F.obj.obj (op V)) : Type u))))) :
                  Type u)) →
              (↑(F.obj.obj (op (U ⊔ V))) : Type u))
          x :
        (↑(F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).obj (op (U ⊔ V))) :
          Type u)) =
    y

Tactic:
refine F.eq_of_locally_eq₂
      (homOfLE (inf_le_right : U ⊓ W ≤ W)) (homOfLE (inf_le_right : V ⊓ W ≤ W)) ?_ _ _ ?_ ?_

Premises used: inf_le_right, TopCat.Sheaf.eq_of_locally_eq₂, CategoryTheory.homOfLE