-- 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
this :
  Eq (α := (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
    ((CommRingCat.Hom.hom
            (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
              Hom.app (I.glueDataObjι U) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) →
            (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
        x :
      (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
    (0 : (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
refine_1 :
  Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    ((CommRingCat.Hom.hom
            ((pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U)
                    (X.homOfLE ⋯)).presheaf.map
              (Quiver.Hom.op (homOfLE ⋯))) :
          (a :
              (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯),
                    (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U) ⁻¹ᵁ
                      (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) :
                Type u)) →
            (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        ((CommRingCat.Hom.hom
                (Hom.app (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))
                  (I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))) :
              (a : (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u)) →
                (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯),
                      (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U) ⁻¹ᵁ
                        (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) :
                  Type u))
            ((CommRingCat.Hom.hom (Hom.app (I.glueDataObjι U) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))) :
                  (a : (↑Γ((↑(↑U : X.Opens) : Scheme), (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u)) →
                    (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
                ((CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                    (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) →
                      (↑Γ((↑(↑U : X.Opens) : Scheme), (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
                  x) :
              (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u)) :
          (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯),
                (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U) ⁻¹ᵁ
                  (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) :
            Type u)) :
      (↑Γ(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
            (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
              Hom.appLE (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U)
                ((↑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))

Tactic:
simp only [Scheme.Opens.ι_app, CommRingCat.hom_comp, RingHom.coe_comp,
        Function.comp_apply, Scheme.Hom.appLE, Scheme.Hom.comp_app, Category.assoc] at this ⊢

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_app, CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Hom.appLE, RingHom.coe_comp, Function.comp_apply, AlgebraicGeometry.Scheme.Opens.ι_app