awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
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))
            a :
          (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) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
f : (↑Γ(X, (↑ia : X.Opens)) : Type u)
g : (↑Γ(X, (↑ib : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
H : (↑((I.glueDataObjι ia) a) : ↥X) ∈ X.basicOpen f
rwa : (↑((I.glueDataObjι ia) a) : ↥X) ∈ X.basicOpen g
rwa₁ rwa₂ rwa₃ rwa₄ : (↑((I.glueDataObjι ia) a) : ↥X) ∈ X.basicOpen f
⊢ (↑((I.glueDataObjι ib) b) : ↥X) ∈ X.basicOpen g

Tactic:
rwa [← this, ← hfg]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
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))
            a :
          (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) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
f : (↑Γ(X, (↑ia : X.Opens)) : Type u)
g : (↑Γ(X, (↑ib : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
H : (↑((I.glueDataObjι ia) a) : ↥X) ∈ X.basicOpen f
⊢ ∀ (W : (↑X.affineOpens : Type u)) (hW : W = X.affineBasicOpen g),
    Membership.mem (γ := Set ↥(I.glueDataObj ib)) (Set.range (ι := ↥(I.glueDataObj W)) ⇑(I.glueDataObjMap ⋯)) b

Tactic:
have hmem (W) (hW : W = X.affineBasicOpen g) :
      b ∈ Set.range (I.glueDataObjMap (hW.trans_le (X.affineBasicOpen_le g))) := by
    subst hW
    refine (I.opensRange_glueDataObjMap g).ge ?_
    change (I.glueDataObjι ib b).1 ∈ X.basicOpen g
    rwa [← this, ← hfg]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
ib : I.glueData.J
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))
            a :
          (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) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
f : (↑Γ(X, (↑ia : X.Opens)) : Type u)
g : (↑Γ(X, (↑ib : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
H : (↑((I.glueDataObjι ia) a) : ↥X) ∈ X.basicOpen f
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
obtain :
  ∀ (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)
⊢ Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) a : ↥I.glueData.glued) ((I.glueData.ι ib) b : ↥I.glueData.glued)

Tactic:
obtain ⟨a, rfl⟩ := (I.opensRange_glueDataObjMap f).ge H

Premises used: Eq.ge, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, rfl
-- 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.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) ((I.glueDataObjMap ⋯) a)) : ↥X)
    (↑((I.glueDataObjι ib) ((I.glueDataObjMap ⋯) b)) : ↥X)
⊢ Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯) a) : ↥X)
    (↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯) b) : ↥X)

Tactic:
simp only [glueData_U, ← Scheme.Hom.comp_apply, glueDataObjMap_glueDataObjι] at this ⊢

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι, AlgebraicGeometry.Scheme.IdealSheafData.glueData_U
-- 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.{u + 1} (α := ↥X) (↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯) a) : ↥X)
    (↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE ⋯) b) : ↥X)
⊢ Eq (α := ↥(X.basicOpen f)) ((I.glueDataObjι (X.affineBasicOpen f)) a : ↥(↑(X.basicOpen f) : Scheme))
    ((I.glueDataObjι (X.affineBasicOpen f)) b : ↥(↑(X.basicOpen f) : Scheme))

Tactic:
simp only [Scheme.affineBasicOpen_coe, Scheme.Hom.comp_base, TopCat.comp_app,
    Scheme.homOfLE_apply, SetLike.coe_eq_coe] at this

Premises used: SetLike.coe_eq_coe, AlgebraicGeometry.Scheme.affineBasicOpen_coe, TopCat.comp_app, AlgebraicGeometry.Scheme.Hom.comp_base, AlgebraicGeometry.Scheme.homOfLE_apply
-- 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
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)

Tactic:
simp only [glueDataObjMap_ι]

Premises used: _private.0.AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_ι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι) =
    (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
(I.range_glueDataObjι_ι U).trans (I.coe_support_inter U).symm

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
⊢ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo = (↑I.support : Set ↥X)

Tactic:
subset_antisymm (Set.range_subset_iff.mpr fun x ↦ ?_) ?_

Premises used: Iff.mpr, subset_antisymm, Set.range_subset_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
refine_1 : ∀ (x : ↥I.glueData.glued), Membership.mem (α := ↥X) (↑I.support : Set ↥X) (I.gluedTo x : ↥X)
refine_2 : (↑I.support : Set ↥X) ⊆ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo
⊢ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo = (↑I.support : Set ↥X)

Tactic:
refine subset_antisymm (Set.range_subset_iff.mpr fun x ↦ ?_) ?_

Premises used: Iff.mpr, subset_antisymm, Set.range_subset_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.glueData.glued
refine_1 :
  ∀ (ix : I.glueData.J) (x : ↥(I.glueDataObj ix)),
    Membership.mem (α := ↥X) (↑I.support : Set ↥X)
      (I.gluedTo
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ix)) :
                (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ix))) →
                  (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
              x :
            (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
        ↥X)
⊢ Membership.mem (α := ↥X) (↑I.support : Set ↥X) (I.gluedTo x : ↥X)

Tactic:
obtain ⟨ix, x : I.glueDataObj ix, rfl⟩ :=
      I.glueData.toGlueData.ι_jointly_surjective forget x

Premises used: AlgebraicGeometry.Scheme.forget, AlgebraicGeometry.Scheme.IdealSheafData.glueData, AlgebraicGeometry.Scheme.GlueData.toGlueData, rfl, CategoryTheory.GlueData.ι_jointly_surjective
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
refine_1 : Membership.mem (α := ↥X) I.support ((I.glueData.ι ix ≫ I.gluedTo) x : ↥X)
⊢ Membership.mem (α := ↥X) (↑I.support : Set ↥X)
    (I.gluedTo
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (forget.map (I.glueData.ι ix)) :
              (a : (fun (X : Type u) ↦ X) (forget.obj (I.glueData.U ix))) →
                (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued))
            x :
          (fun (X : Type u) ↦ X) (forget.obj I.glueData.glued)) :
      ↥X)

Tactic:
change (I.glueData.ι _ ≫ I.gluedTo) x ∈ I.support

Premises used: AlgebraicGeometry.Scheme.GlueData.ι, AlgebraicGeometry.Scheme.IdealSheafData.support, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.IdealSheafData.glueData, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.IdealSheafData.gluedTo, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
refine_1 : Membership.mem (α := ↥X) I.support ((I.glueDataObjι ix ≫ (↑ix : X.Opens).ι) x : ↥X)
⊢ Membership.mem (α := ↥X) I.support ((I.glueData.ι ix ≫ I.gluedTo) x : ↥X)

Tactic:
rw [ι_gluedTo]

Premises used: _private.0.AlgebraicGeometry.Scheme.IdealSheafData.ι_gluedTo
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ Membership.mem (α := ↥X) I.support ((I.glueDataObjι ix ≫ (↑ix : X.Opens).ι) x : ↥X)

Tactic:
((I.range_glueDataObjι_ι_eq_support_inter ix).le ⟨_, rfl⟩).1

Premises used: Set.Mem, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, Eq.le, And.left, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ Membership.mem (α := ↥X) I.support ((I.glueDataObjι ix ≫ (↑ix : X.Opens).ι) x : ↥X)

Tactic:
exact ((I.range_glueDataObjι_ι_eq_support_inter ix).le ⟨_, rfl⟩).1

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, Eq.le, And.left, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
hx : x ∈ (↑I.support : Set ↥X)
refine_2 :
  ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)),
    Membership.mem (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo) x
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo) x

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
hx : x ∈ (↑I.support : Set ↥X)
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
refine_2 :
  ∀ (y : ↥(I.glueDataObj (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU)))
    (hx :
      Membership.mem (α := ↥X) (↑I.support : Set ↥X)
        ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
            y :
          ↥X))
    (hxU :
      Membership.mem (α := ↥X) (↑U : Set ↥X)
        ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
            y :
          ↥X)),
    Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
      ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
          y :
        ↥X)
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo) x

Tactic:
obtain ⟨y, rfl⟩ := (I.range_glueDataObjι_ι_eq_support_inter ⟨U, hU⟩).ge ⟨hx, hxU⟩

Premises used: Eq.ge, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter, Subtype.mk, And.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU))
hx :
  Membership.mem (α := ↥X) (↑I.support : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
hxU :
  Membership.mem (α := ↥X) (↑U : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
refine_2 :
  Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
    ((I.glueData.ι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫ I.gluedTo) y : ↥X)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)

Tactic:
rw [← ι_gluedTo]

Premises used: _private.0.AlgebraicGeometry.Scheme.IdealSheafData.ι_gluedTo
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU))
hx :
  Membership.mem (α := ↥X) (↑I.support : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
hxU :
  Membership.mem (α := ↥X) (↑U : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
    ((I.glueData.ι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫ I.gluedTo) y : ↥X)

Tactic:
⟨_, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU))
hx :
  Membership.mem (α := ↥X) (↑I.support : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
hxU :
  Membership.mem (α := ↥X) (↑U : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
    ((I.glueData.ι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫ I.gluedTo) y : ↥X)

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
simp :
  Eq (α := Set ↥I.glueData.glued) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U))
    (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
⊢ Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U) = (↑(I.gluedTo ⁻¹ᵁ (↑U : X.Opens)) : Set ↥I.glueData.glued)

Tactic:
simp only [TopologicalSpace.Opens.map_coe]

Premises used: TopologicalSpace.Opens.map_coe
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
⊢ Eq (α := Set ↥I.glueData.glued) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U))
    (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))

Tactic:
apply I.gluedTo_injective.image_injective

Premises used: _private.0.AlgebraicGeometry.Scheme.IdealSheafData.gluedTo_injective, Function.Injective.image_injective