-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
ia ib : I.glueData.J
b : ↥(I.glueDataObj ib)
f : (↑Γ(X, (↑ia : X.Opens)) : Type u)
g : (↑Γ(X, (↑ib : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hmem :
  ∀ (W : (↑X.affineOpens : Type u)) (hW : W = X.affineBasicOpen g),
    Membership.mem (γ := Set ↥(I.glueDataObj ib)) (Set.range (ι := ↥(I.glueDataObj W)) ⇑(I.glueDataObjMap ⋯)) b
a : ↥(I.glueDataObj (X.affineBasicOpen f))
e :
  Eq (α := ↥X)
    (I.gluedTo
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
                (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
            ((I.glueDataObjMap ⋯) a : ↥(I.glueDataObj ia)) :
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
      ↥X)
    (I.gluedTo
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ib)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ib))) →
                (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
            b :
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
      ↥X)
this : Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
H : (↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) : ↥X) ∈ X.basicOpen f
⊢ Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) ((I.glueDataObjMap ⋯) a : ↥(I.glueDataObj ia)) : ↥I.glueData.glued)
    ((I.glueData.ι ib) b : ↥I.glueData.glued)
have obtain : ∀ (b : ↥(I.glueDataObj (X.affineBasicOpen f)))
  (hmem :
    ∀ (W : (↑X.affineOpens : Type u)) (hW : W = X.affineBasicOpen g),
      Membership.mem (α := ↥(I.glueDataObj ib)) (γ := Set ↥(I.glueDataObj ib))
        (Set.range (ι := ↥(I.glueDataObj W)) ⇑(I.glueDataObjMap sorry)) ((I.glueDataObjMap sorry) b : ↥(I.glueDataObj ib)))
  (e :
    Eq (α := ↥X)
      (I.gluedTo
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ia)) :
                (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ia))) →
                  (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
              ((I.glueDataObjMap sorry) a : ↥(I.glueDataObj ia)) :
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
        ↥X)
      (I.gluedTo
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ib)) :
                (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ib))) →
                  (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
              ((I.glueDataObjMap sorry) b : ↥(I.glueDataObj ib)) :
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
        ↥X))
  (this :
    Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) ((I.glueDataObjMap sorry) a)) : ↥X)
      (↑((I.glueDataObjι ib) ((I.glueDataObjMap sorry) b)) : ↥X)),
  Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) ((I.glueDataObjMap sorry) a : ↥(I.glueDataObj ia)) : ↥I.glueData.glued)
    ((I.glueData.ι ib) ((I.glueDataObjMap sorry) b : ↥(I.glueDataObj ib)) : ↥I.glueData.glued)
Tactic: obtain ⟨b, rfl⟩ := hmem (X.affineBasicOpen f) (Subtype.ext hfg)
Cleared hypotheses: b, hmem, e, this