-- 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:
X : TopCat
F : Sheaf CommRingCat X
U V W UW VW : 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))
h₁ : UW = U ⊓ W
h₂ : VW = V ⊓ W
⊢ (ConcreteCategory.hom (F.val.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y ↔
    (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y ∧
      (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y

Tactic:
subst h₁ h₂

Result:
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))
⊢ (ConcreteCategory.hom (F.val.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y ↔
    (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).1 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y ∧
      (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) (↑x).2 = (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op)) y

Proof state:
case mpr.intro.refine_2
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))

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

Result:
no goals

Proof state:
case mpr.intro
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 e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) = y

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

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 ⊓ W ⊔ V ⊓ W

case mpr.intro.refine_2
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

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