-- 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)
⊢ 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))
          ((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 ⊔ V)))
                  (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
                    (Quiver.Hom.op (homOfLE ⋯))) :
                (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u)) → (↑(F.obj.obj (op U)) : 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 U)) :
              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))
          ((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)) ∧
    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))
          ((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 ⊔ V)))
                  (F.obj (P := CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑X : Type u))).map
                    (Quiver.Hom.op (homOfLE ⋯))) :
                (a : (↑(F.obj.obj (op (U ⊔ V))) : Type u)) → (↑(F.obj.obj (op V)) : 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 V)) :
              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))
          ((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))

Tactic:
simp only [← CommRingCat.comp_apply, ← Functor.map_comp, ← op_comp,
      homOfLE_comp, and_self]

Premises used: CategoryTheory.op_comp, and_self, CategoryTheory.homOfLE_comp, CommRingCat.comp_apply, CategoryTheory.Functor.map_comp