-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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))
⊢ 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))
have refine_1 : Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  ((CommRingCat.Hom.hom
          ((pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE sorry)).presheaf.map
            (Quiver.Hom.op (homOfLE sorry))) :
        (a :
            (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry),
                  (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U) ⁻¹ᵁ
                    (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) :
              Type u)) →
          (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
      ((CommRingCat.Hom.hom
              (Hom.app (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry))
                (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 sorry),
                    (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ 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 sorry))) :
                  (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 sorry),
              (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U) ⁻¹ᵁ
                (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) :
          Type u)) :
    (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : 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 ⊢