-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ia ib : I.glueData.J
f : (↑Γ(X, (↑ia : X.Opens)) : Type u)
g : (↑Γ(X, (↑ib : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
a : ↥(I.glueDataObj (X.affineBasicOpen f))
H : (↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) : ↥X) ∈ X.basicOpen f
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 (α := ↥(X.basicOpen f)) ((I.glueDataObjι (X.affineBasicOpen f)) a : ↥(↑(X.basicOpen f) : Scheme))
    ((I.glueDataObjι (X.affineBasicOpen f)) b : ↥(↑(X.basicOpen f) : Scheme))
obtain :
  ∀
    (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 ⋯) a : ↥(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 ⋯) a : ↥(I.glueDataObj ib)) :
              (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
          ↥X))
    (this :
      Eq (α := ↥(X.basicOpen f)) ((I.glueDataObjι (X.affineBasicOpen f)) a : ↥(↑(X.basicOpen f) : Scheme))
        ((I.glueDataObjι (X.affineBasicOpen f)) a : ↥(↑(X.basicOpen f) : Scheme))),
    Eq (α := ↥I.glueData.glued) ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ia) a : ↥I.glueData.glued)
      ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ib) a : ↥I.glueData.glued)
⊢ Eq (α := ↥I.glueData.glued) ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ia) a : ↥I.glueData.glued)
    ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ib) b : ↥I.glueData.glued)

Tactic:
obtain rfl := (I.glueDataObjι (X.affineBasicOpen f)).isEmbedding.injective this

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, AlgebraicGeometry.Scheme.affineBasicOpen, AlgebraicGeometry.Scheme.Hom.isEmbedding, Topology.IsEmbedding.injective, rfl