-- 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_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

Tactic:
rw [← e₁, ← TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst]

Result:
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))

Proof state:
case mp
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))))))
⊢ (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.val.map (homOfLE ⋯).op))
          ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x)) =
      (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)) =
      (ConcreteCategory.hom (F.val.map (homOfLE ⋯).op))
        ((ConcreteCategory.hom (F.val.map (homOfLE e).op)) ((ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x))

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

Result:
no goals

Proof state:
case mp
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

Tactic:
rintro rfl

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

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))
      ((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