awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
⊢ ∀ (a : (MultispanShape.prod I.glueData.J).L),
    Eq (α := I.glueData.diagram.left a ⟶ X)
      (I.glueData.diagram.fst a ≫
        (fun (i : (MultispanShape.prod I.glueData.J).R) ↦ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
          ((MultispanShape.prod I.glueData.J).fst a))
      (I.glueData.diagram.snd a ≫
        (fun (i : (MultispanShape.prod I.glueData.J).R) ↦ I.glueDataObjι i ≫ (↑i : X.Opens).ι)
          ((MultispanShape.prod I.glueData.J).snd a))

Tactic:
simp [GlueData.diagram, pullback.condition_assoc]

Premises used: CategoryTheory.GlueData.diagram, CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ I.glueData.ι U ≫ I.gluedTo = I.glueDataObjι U ≫ (↑U : X.Opens).ι

Tactic:
Multicoequalizer.π_desc _ _ _ _ _

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj, CategoryTheory.Limits.Multicoequalizer.π_desc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ (↑U : X.Opens) ≤ (↑U : X.Opens) ⊓ (↑V : X.Opens)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 (↑(↑U : X.Opens) : Scheme)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)

Tactic:
have : IsIso (X.homOfLE inf_le_left : (U.1 ⊓ V.1).toScheme ⟶ U) :=
    ⟨X.homOfLE (by simpa), by simp, by simp⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
⊢ (↑U : X.Opens) ≤ (↑U : X.Opens) ⊓ (↑V : X.Opens)

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
rw : X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)
⊢ inv (X.homOfLE ⋯) = X.homOfLE ⋯

Tactic:
rw [eq_comm, ← hom_comp_eq_id]

Premises used: CategoryTheory.hom_comp_eq_id, eq_comm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
⊢ inv (X.homOfLE ⋯) = X.homOfLE ⋯

Tactic:
have H : inv (X.homOfLE inf_le_left : (U.1 ⊓ V.1).toScheme ⟶ U) = X.homOfLE (by simpa) := by
    rw [eq_comm, ← hom_comp_eq_id]; simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
⊢ I.glueData.t U V ≫ I.glueData.f V U ≫ I.glueData.ι V = I.glueData.f U V ≫ I.glueData.ι U

Tactic:
have := I.glueData.glue_condition U V
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObjPullback U V ⟶ I.glueData.glued)
    (I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueData.ι U)
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)

Tactic:
rw [← IsIso.inv_comp_eq] at this

Premises used: CategoryTheory.IsIso.inv_comp_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)
rw :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V)
    (𝟙 (I.glueData.U U) ≫
      inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V) (I.glueData.ι U)

Tactic:
rw [← Category.id_comp (I.glueData.ι U), ← this]

Premises used: AlgebraicGeometry.Scheme.GlueData.ι, AlgebraicGeometry.Scheme.IdealSheafData.glueData, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)
e_a :
  I.glueDataObjMap h =
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
      pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)
⊢ Eq (α := I.glueDataObj U ⟶ I.glueData.glued) (I.glueDataObjMap h ≫ I.glueData.ι V)
    (𝟙 (I.glueData.U U) ≫
      ((inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
          pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
        I.glueData.ι V)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)
e_a :
  I.glueDataObjMap h ≫ I.glueDataObjι V =
    ((inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
        pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
      I.glueDataObjι V
⊢ I.glueDataObjMap h =
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
      pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _)]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.cancel_mono
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
this_1 : IsIso (X := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  Eq (α := I.glueDataObj U ⟶ I.glueData.glued)
    (inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V)
    (I.glueData.ι U)
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V =
    ((inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫ I.glueDataT U V) ≫
        pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
      I.glueDataObjι V

Tactic:
simp [pullback_inv_fst_snd_of_right_isIso_assoc, H]

Premises used: CategoryTheory.Limits.pullback_inv_fst_snd_of_right_isIso_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
a b : ↥I.glueData.glued
e : Eq (α := ↥X) (I.gluedTo a : ↥X) (I.gluedTo b : ↥X)
obtain :
  ∀ (ia : I.glueData.J) (a : ↥(I.glueDataObj ia))
    (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 b : ↥X)),
    (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 =
      b
⊢ a = b

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

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
b : ↥I.glueData.glued
ia : I.glueData.J
a : ↥(I.glueDataObj ia)
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 b : ↥X)
obtain :
  ∀ (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)
      ((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))
      ((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))
⊢ (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 =
    b

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

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
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 (α := ↥X) ((I.glueData.ι ia ≫ I.gluedTo) a : ↥X) ((I.glueData.ι ib ≫ I.gluedTo) b : ↥X)

Tactic:
have : (I.glueData.ι ia ≫ I.gluedTo) a = (I.glueData.ι ib ≫ I.gluedTo) b := e
-- 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 (α := ↥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)
rwa₁ rwa₂ rwa₃ 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)
⊢ Eq.{u + 1} (α := ↥X) (↑((I.glueDataObjι ia) a) : ↥X) (↑((I.glueDataObjι ib) b) : ↥X)

Tactic:
rwa [ι_gluedTo, ι_gluedTo] at this

Premises used: _private.0.AlgebraicGeometry.Scheme.IdealSheafData.ι_gluedTo
-- 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)
⊢ 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
-- 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)
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)
⊢ 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⟩

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.ConcreteCategory.hom, Eq.rec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.exists_basicOpen_le_affine_inter, Eq.symm, Subtype.val, DFunLike.coe, Subtype.property
-- 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
subst :
  Membership.mem (γ := Set ↥(I.glueDataObj ib))
    (Set.range (ι := ↥(I.glueDataObj (X.affineBasicOpen g))) ⇑(I.glueDataObjMap ⋯)) b
⊢ Membership.mem (γ := Set ↥(I.glueDataObj ib)) (Set.range (ι := ↥(I.glueDataObj W)) ⇑(I.glueDataObjMap ⋯)) b

Tactic:
subst hW
-- 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
⊢ Membership.mem (γ := Set ↥(I.glueDataObj ib))
    (Set.range (ι := ↥(I.glueDataObj (X.affineBasicOpen g))) ⇑(I.glueDataObjMap ⋯)) b

Tactic:
(I.opensRange_glueDataObjMap g).ge ?_

Premises used: Eq.ge, Set.Mem, setOf, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap, Set.range
-- 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
refine : b ∈ I.glueDataObjι ib ⁻¹ᵁ (↑ib : X.Opens).ι ⁻¹ᵁ X.basicOpen g
⊢ Membership.mem (γ := Set ↥(I.glueDataObj ib))
    (Set.range (ι := ↥(I.glueDataObj (X.affineBasicOpen g))) ⇑(I.glueDataObjMap ⋯)) b

Tactic:
refine (I.opensRange_glueDataObjMap g).ge ?_

Premises used: Eq.ge, AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap
-- 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
change : (↑((I.glueDataObjι ib) b) : ↥X) ∈ X.basicOpen g
⊢ b ∈ I.glueDataObjι ib ⁻¹ᵁ (↑ib : X.Opens).ι ⁻¹ᵁ X.basicOpen g

Tactic:
change (I.glueDataObjι ib b).1 ∈ X.basicOpen g

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, Subtype.val, DFunLike.coe