-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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
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 ⋯)) ((I.glueDataObjMap ⋯) 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 ⋯) 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 ⋯) 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 ⋯) a)) : ↥X)
        (↑((I.glueDataObjι ib) ((I.glueDataObjMap ⋯) b)) : ↥X)),
    Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) ((I.glueDataObjMap ⋯) a : ↥(I.glueDataObj ia)) : ↥I.glueData.glued)
      ((I.glueData.ι ib) ((I.glueDataObjMap ⋯) b : ↥(I.glueDataObj ib)) : ↥I.glueData.glued)
⊢ Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) ((I.glueDataObjMap ⋯) a : ↥(I.glueDataObj ia)) : ↥I.glueData.glued)
    ((I.glueData.ι ib) b : ↥I.glueData.glued)

Tactic:
obtain ⟨b, rfl⟩ := hmem (X.affineBasicOpen f) (Subtype.ext hfg)

Premises used: AlgebraicGeometry.Scheme.affineBasicOpen, rfl, Subtype.ext