-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
h :
  Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
      Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
        CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
            Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
          (Hom.app F ⊤ :
            Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
              Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) =
    Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯
refine_1 :
  Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    ((CommRingCat.Hom.hom
            (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
              Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        x :
      (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
⊢ Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (((CommRingCat.Hom.hom
              (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
                Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
                  CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
                    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
                      Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
                    (Hom.app F ⊤ :
                      Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                        Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤))) :
            (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u)) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        x :
      (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))

Tactic:
convert_to (U.1.ι.app V.1 ≫ (F ≫ X.homOfLE inf_le_left).appLE (U.1.ι ⁻¹ᵁ V.1) ⊤
      (by rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]
          exact fun x _ ↦ by simpa using (F x).2.2)).hom x = 0 using 3

Premises used: AlgebraicGeometry.Scheme.homOfLE, CommRingCat.Hom.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.app, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, inf_le_left, Top.top, Subtype.val, DFunLike.coe, CategoryTheory.Functor.obj