awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
f' : (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V :=
  (Ideal.Quotient.mk (I.ideal V) :
      (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    f
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
⊢ (↑((Opens.comap
                { toFun := comap (Ideal.Quotient.mk (I.ideal V)), continuous_toFun := ⋯ :
                  C(PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V),
                    PrimeSpectrum (↑Γ(X, (↑V : X.Opens)) : Type u)) } :
              (a : TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, (↑V : X.Opens)) : Type u))) →
                TopologicalSpace.Opens (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)))
            (IsAffineOpen.fromSpec ⋯ ⁻¹ᵁ X.basicOpen f) :
          TopologicalSpace.Opens (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) :
      Set (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) =
    (↑((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ X.basicOpen f) :
      Set ↥(I.glueDataObj V))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
rw :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h

Tactic:
rw [glueDataObjMap, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.quotientMap_comp_mk, CommRingCat.ofHom_comp, Spec.map_comp_assoc, glueDataObjι,
    Category.assoc]

Premises used: CategoryTheory.Category.assoc, Ideal.quotientMap_comp_mk, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, AlgebraicGeometry.Spec.map_comp_assoc, CommRingCat.ofHom_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
e_a :
  Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
e_a : (↑U : X.Opens).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
⊢ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h

Tactic:
rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom, CommRingCat.ofHom_hom]

Premises used: CommRingCat.ofHom_hom, CategoryTheory.Iso.eq_inv_comp, AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
e_a : X.homOfLE h ≫ (↑V : X.Opens).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
⊢ (↑U : X.Opens).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h

Tactic:
erw [Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc U.1 V.1 h]

Premises used: AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
e_a : X.homOfLE h ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
e_a₁ : X.homOfLE h ≫ 𝟙 (↑(↑V : X.Opens) : Scheme) = X.homOfLE h
e_a₂ e_a₃ : X.homOfLE h = X.homOfLE h
⊢ X.homOfLE h ≫ (↑V : X.Opens).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h

Tactic:
rw [← IsAffineOpen.isoSpec_hom V.2, Iso.hom_inv_id, Category.comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ (↑U : X.Opens) ⊓ (↑V : X.Opens) ≤ (↑V : X.Opens) ⊓ (↑U : X.Opens)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
refine_1 :
  I.ideal V ≤
    RingHom.ker
      (CommRingCat.Hom.hom
        (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫ Hom.appTop (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)))
refine_2 :
  Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V =
    (F ≫ X.homOfLE ⋯) ≫ X.homOfLE ⋯
⊢ I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U

Tactic:
refine pullback.lift ((F ≫ X.homOfLE inf_le_right ≫
    V.2.isoSpec.hom).liftQuotient _ ?_) (F ≫ X.homOfLE (by simp)) ?_

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.Scheme.homOfLE, CategoryTheory.Limits.pullback.lift, inf_le_right, AlgebraicGeometry.Scheme.Hom.liftQuotient, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
refine_1 :
  Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (((CommRingCat.Hom.hom
              (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
                Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
                  CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
                    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
                      Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
                    (Hom.app F ⊤ :
                      Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                        Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤))) :
            (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u)) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        x :
      (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
⊢ Membership.mem (γ := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫ Hom.appTop (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom))))
    x

Tactic:
simp only [Hom.comp_app, Hom.comp_base, TopologicalSpace.Opens.map_comp_obj,
      TopologicalSpace.Opens.map_top, homOfLE_app, homOfLE_leOfHom, Category.assoc, RingHom.mem_ker]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_app, RingHom.mem_ker, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Scheme.homOfLE_app, TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
rw : ⊤ ≤ (F ≫ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι) ⁻¹ᵁ (↑V : X.Opens)
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯) ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)

Tactic:
rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.Scheme.Hom.comp_preimage
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x_1 : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x_1 ∈ I.ideal V
x : ↥(pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯))
h :
  Membership.mem (γ :=
    TopologicalSpace.Opens
      ↥(pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯)))
    ⊤ x
⊢ x ∈ (F ≫ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι) ⁻¹ᵁ (↑V : X.Opens)

Tactic:
simpa using (F x).2.2

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.right, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι) ⁻¹ᵁ (↑V : X.Opens)

Tactic:
exact fun x _ ↦ by simpa using (F x).2.2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
h :
  Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
        Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
          CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
              Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
            (Hom.app F ⊤ :
              Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (CategoryStruct.comp (Y := Γ((↑(↑U : X.Opens) : Scheme), (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
        (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
        (CategoryStruct.comp (Y :=
          Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
          (Hom.appLE F (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
⊢ Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
      Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
        CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
            Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
          (Hom.app F ⊤ :
            Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
              Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) =
    Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯

Tactic:
simp only [homOfLE_leOfHom, Opens.ι_app, Hom.comp_appLE, homOfLE_app]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_appLE, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Scheme.homOfLE_app, AlgebraicGeometry.Scheme.Opens.ι_app
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
rw : ⊤ ≤ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ⁻¹ᵁ (↑V : X.Opens)
⊢ LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))

Tactic:
rw [← Scheme.Hom.comp_preimage, X.homOfLE_ι]

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.Scheme.Hom.comp_preimage
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x_1 : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x_1 ∈ I.ideal V
x : ↥(↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)
h : Membership.mem (γ := TopologicalSpace.Opens ↥(↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) ⊤ x
⊢ x ∈ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ⁻¹ᵁ (↑V : X.Opens)

Tactic:
simpa using x.2.2

Premises used: And.right, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ⁻¹ᵁ (↑V : X.Opens)

Tactic:
exact fun x _ ↦ by simpa using x.2.2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))

Tactic:
have H : ⊤ ≤ X.homOfLE (inf_le_left (b := V.1)) ⁻¹ᵁ U.1.ι ⁻¹ᵁ V.1 := by
        rw [← Scheme.Hom.comp_preimage, X.homOfLE_ι]; exact fun x _ ↦ by simpa using x.2.2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
H :
  LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))
h :
  Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
        Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
          CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
              Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
            (Hom.app F ⊤ :
              Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
        X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
          (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).presheaf.map (homOfLE H).op ≫ Hom.appLE F ⊤ ⊤ ⋯ :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
⊢ Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
        Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
          CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
              Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
            (Hom.app F ⊤ :
              Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (CategoryStruct.comp (Y := Γ((↑(↑U : X.Opens) : Scheme), (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
        (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
        (CategoryStruct.comp (Y :=
          Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
          (Hom.appLE F (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))

Tactic:
rw [← F.map_appLE (show ⊤ ≤ F ⁻¹ᵁ ⊤ from le_rfl) (homOfLE H).op]

Premises used: le_rfl, Quiver.Hom.op, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Hom.map_appLE
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
H :
  LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))
h :
  Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (CategoryStruct.comp (Y := Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
        (X.presheaf.map (eqToHom ⋯ ≫ Quiver.Hom.op (homOfLE ⋯)) :
          Γ(X, (↑V : X.Opens)) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
        (Hom.appLE F ⊤ (F ⁻¹ᵁ ⊤) ⋯ :
          Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) ≫
        Hom.appLE F ⊤ ⊤ ⋯ :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
⊢ Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
        Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
          CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
              Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
            (Hom.app F ⊤ :
              Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
        X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
          (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).presheaf.map (homOfLE H).op ≫ Hom.appLE F ⊤ ⊤ ⋯ :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))

Tactic:
simp only [homOfLE_leOfHom, Opens.toScheme_presheaf_map, Quiver.Hom.unop_op,
        Hom.opensFunctor_map_homOfLE, ← Functor.map_comp_assoc, IsAffineOpen.isoSpec_hom_appTop,
        Opens.topIso_inv, eqToHom_op, homOfLE_leOfHom, Category.assoc,
        Iso.inv_hom_id_assoc, F.app_eq_appLE]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Opens.topIso_inv, AlgebraicGeometry.Scheme.Hom.opensFunctor_map_homOfLE, Quiver.Hom.unop_op, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.homOfLE_leOfHom, CategoryTheory.eqToHom_op, CategoryTheory.Functor.map_comp_assoc, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_map, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
H :
  LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))
⊢ Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (CategoryStruct.comp (Y := Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
        (X.presheaf.map (eqToHom ⋯ ≫ Quiver.Hom.op (homOfLE ⋯)) :
          Γ(X, (↑V : X.Opens)) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
        (Hom.appLE F ⊤ (F ⁻¹ᵁ ⊤) ⋯ :
          Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (homOfLE ⋯)) ≫
        Hom.appLE F ⊤ ⊤ ⋯ :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))

Tactic:
rfl