awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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 (α := ↥X) ((I.glueData.ι ia ≫ I.gluedTo) a : ↥X) ((I.glueData.ι ib ≫ I.gluedTo) b : ↥X)
⊢ Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
have rwa : ∀ (this : Eq (α := ↥X) ((I.glueDataObjι ia ≫ (↑ia : X.Opens).ι) a : ↥X) ((I.glueData.ι ib ≫ I.gluedTo) b : ↥X)),
  Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
Tactic: rwa [ι_gluedTo, ι_gluedTo] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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 (α := ↥X) ((I.glueData.ι ia ≫ I.gluedTo) a : ↥X) ((I.glueData.ι ib ≫ I.gluedTo) b : ↥X)
rwa :
  ∀ (this : Eq (α := ↥X) ((I.glueDataObjι ia ≫ (↑ia : X.Opens).ι) a : ↥X) ((I.glueData.ι ib ≫ I.gluedTo) b : ↥X)),
    Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
⊢ Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
have rwa₁ : ∀
  (this :
    Eq (α := ↥X) ((I.glueDataObjι ia ≫ (↑ia : X.Opens).ι) a : ↥X) ((I.glueDataObjι ib ≫ (↑ib : X.Opens).ι) b : ↥X)),
  Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
Tactic: rwa [ι_gluedTo, ι_gluedTo] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
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)
⊢ Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) a : ↥I.glueData.glued) ((I.glueData.ι ib) b : ↥I.glueData.glued)
have this : Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)
Tactic: have : (I.glueDataObjι ia a).1 = (I.glueDataObjι ib b).1 := by
    have : (I.glueData.ι ia ≫ I.gluedTo) a = (I.glueData.ι ib ≫ I.gluedTo) b := e
    rwa [ι_gluedTo, ι_gluedTo] at this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
⊢ Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) a : ↥I.glueData.glued) ((I.glueData.ι ib) b : ↥I.glueData.glued)
have obtain : ∀ (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),
  Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) a : ↥I.glueData.glued) ((I.glueData.ι ib) b : ↥I.glueData.glued)
Tactic: obtain ⟨f, g, hfg, H⟩ := exists_basicOpen_le_affine_inter ia.2 ib.2
    (I.glueDataObjι ia a).1
      ⟨(I.glueDataObjι ia a).2, this ▸ (I.glueDataObjι ib b).2⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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
have subst : Membership.mem (γ := Set ↥(I.glueDataObj ib))
  (Set.range (ι := ↥(I.glueDataObj (X.affineBasicOpen g))) ⇑(I.glueDataObjMap sorry)) b
Tactic: subst hW
Cleared hypotheses: W, hW
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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
⊢ Membership.mem (γ := Set ↥(I.glueDataObj ib))
    (Set.range (ι := ↥(I.glueDataObj (X.affineBasicOpen g))) ⇑(I.glueDataObjMap ⋯)) b
have refine : b ∈ I.glueDataObjι ib ⁻¹ᵁ (↑ib : X.Opens).ι ⁻¹ᵁ X.basicOpen g
Tactic: refine (I.opensRange_glueDataObjMap g).ge ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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
⊢ b ∈ I.glueDataObjι ib ⁻¹ᵁ (↑ib : X.Opens).ι ⁻¹ᵁ X.basicOpen g
have change : (↑((I.glueDataObjι ib) b) : ↥X) ∈ X.basicOpen g
Tactic: change (I.glueDataObjι ib b).1 ∈ X.basicOpen g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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
⊢ (↑((I.glueDataObjι ib) b) : ↥X) ∈ X.basicOpen g
have rwa : (↑((I.glueDataObjι ia) a) : ↥X) ∈ X.basicOpen g
Tactic: rwa [← this, ← hfg]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
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
⊢ Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) a : ↥I.glueData.glued) ((I.glueData.ι ib) b : ↥I.glueData.glued)
have hmem : ∀ (W : (↑X.affineOpens : Type u)) (hW : W = X.affineBasicOpen g),
  Membership.mem (γ := Set ↥(I.glueDataObj ib)) (Set.range (ι := ↥(I.glueDataObj W)) ⇑(I.glueDataObjMap sorry)) 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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
⊢ Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) a : ↥I.glueData.glued) ((I.glueData.ι ib) b : ↥I.glueData.glued)
have 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 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))
              b :
            (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) b) : ↥X))
  (H : (↑((I.glueDataObjι ia) ((I.glueDataObjMap sorry) a)) : ↥X) ∈ X.basicOpen f),
  Eq (α := ↥I.glueData.glued) ((I.glueData.ι ia) ((I.glueDataObjMap sorry) a : ↥(I.glueDataObj ia)) : ↥I.glueData.glued)
    ((I.glueData.ι ib) b : ↥I.glueData.glued)
Tactic: obtain ⟨a, rfl⟩ := (I.opensRange_glueDataObjMap f).ge H
Cleared hypotheses: a, e, this, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
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 (α := ↥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)
have this₁ : Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE sorry) a) : ↥X)
  (↑((I.glueDataObjι (X.affineBasicOpen f) ≫ X.homOfLE sorry) b) : ↥X)
Tactic: simp only [glueData_U, ← Scheme.Hom.comp_apply, glueDataObjMap_glueDataObjι] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
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 (α := ↥I.glueData.glued) ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ia) a : ↥I.glueData.glued)
    ((I.glueDataObjMap ⋯ ≫ I.glueData.ι ib) b : ↥I.glueData.glued)
have 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))
Tactic: simp only [Scheme.affineBasicOpen_coe, Scheme.Hom.comp_base, TopCat.comp_app,
    Scheme.homOfLE_apply, SetLike.coe_eq_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo = (↑I.support : Set ↥X)
have refine_1 : ∀ (x : ↥I.glueData.glued), Membership.mem (α := ↥X) (↑I.support : Set ↥X) (I.gluedTo x : ↥X)
Tactic: refine subset_antisymm (Set.range_subset_iff.mpr fun x ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
refine_1 : ∀ (x : ↥I.glueData.glued), Membership.mem (α := ↥X) (↑I.support : Set ↥X) (I.gluedTo x : ↥X)
⊢ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo = (↑I.support : Set ↥X)
have refine_2 : (↑I.support : Set ↥X) ⊆ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo
Tactic: refine subset_antisymm (Set.range_subset_iff.mpr fun x ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.glueData.glued
⊢ Membership.mem (α := ↥X) (↑I.support : Set ↥X) (I.gluedTo x : ↥X)
have 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)
Tactic: obtain ⟨ix, x : I.glueDataObj ix, rfl⟩ :=
      I.glueData.toGlueData.ι_jointly_surjective forget x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
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)
have refine_1 : Membership.mem (α := ↥X) I.support ((I.glueData.ι ix ≫ I.gluedTo) x : ↥X)
Tactic: change (I.glueData.ι _ ≫ I.gluedTo) x ∈ I.support
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
ix : I.glueData.J
x : ↥(I.glueDataObj ix)
⊢ Membership.mem (α := ↥X) I.support ((I.glueData.ι ix ≫ I.gluedTo) x : ↥X)
have refine_1 : Membership.mem (α := ↥X) I.support ((I.glueDataObjι ix ≫ (↑ix : X.Opens).ι) x : ↥X)
Tactic: rw [ι_gluedTo]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
hx : x ∈ (↑I.support : Set ↥X)
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo) x
have 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
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ