-- Mathlib/Topology/Sheaves/CommRingCat.lean
theorem objSupIsoProdEqLocus_inv_eq_iff {X : TopCat.{u}} (F : X.Sheaf CommRingCat.{u})
    {U V W UW VW : Opens X} (e : W ≤ U ⊔ V) (x) (y : F.1.obj (op W))
    (h₁ : UW = U ⊓ W) (h₂ : VW = V ⊓ W) :
    F.1.map (homOfLE e).op ((F.objSupIsoProdEqLocus U V).inv x) = y ↔
    F.1.map (homOfLE (h₁ ▸ inf_le_left : UW ≤ U)).op x.1.1 =
      F.1.map (homOfLE <| h₁ ▸ inf_le_right).op y ∧
    F.1.map (homOfLE (h₂ ▸ inf_le_left : VW ≤ V)).op x.1.2 =
      F.1.map (homOfLE <| h₂ ▸ inf_le_right).op y

Proof state:
case mpr.intro.refine_3
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.val.obj (op U)) ↑(F.val.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.val.obj (op U)) ↑(F.val.obj (op V))))))
y : ↑(F.val.obj (op W))
e₁ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.val.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y

Tactic:
rw [← e₂, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd]

Result:
case mpr.intro.refine_3
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.val.obj (op U)) ↑(F.val.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.val.obj (op U)) ↑(F.val.obj (op V))))))
y : ↑(F.val.obj (op W))
e₁ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
⊢ (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.val.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
    (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op))
      ((ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))

Proof state:
case mpr.intro.refine_1
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.val.obj (op U)) ↑(F.val.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.val.obj (op U)) ↑(F.val.obj (op V))))))
y : ↑(F.val.obj (op W))
e₁ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
⊢ W ≤ U ⊓ W ⊔ V ⊓ W

Tactic:
rw [← inf_sup_right]

Result:
case mpr.intro.refine_1
X : TopCat
F : Sheaf CommRingCat X
U V W : Opens ↑X
e : W ≤ U ⊔ V
x :
  ↑(CommRingCat.of
      ↥(((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
              (RingHom.fst ↑(F.val.obj (op U)) ↑(F.val.obj (op V)))).eqLocus
          ((CommRingCat.Hom.hom (F.val.map (homOfLE ⋯).op)).comp
            (RingHom.snd ↑(F.val.obj (op U)) ↑(F.val.obj (op V))))))
y : ↑(F.val.obj (op W))
e₁ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
e₂ : (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y
⊢ W ≤ (U ⊔ V) ⊓ W