-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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))
⊢ Eq (α := ↥I.glueData.glued) ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ia) a : ↥I.glueData.glued)
    ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ib) b : ↥I.glueData.glued)
have 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 sorry)) ((I.glueDataObjMap sorry) 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 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) 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 sorry ≫ I.glueData.ι ia) a : ↥I.glueData.glued)
    ((I.glueDataObjMap sorry ≫ I.glueData.ι ib) a : ↥I.glueData.glued)
Tactic: obtain rfl := (I.glueDataObjι (X.affineBasicOpen f)).isEmbedding.injective this
Cleared hypotheses: b, hmem, e, this