awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ X.nilradical.support = ⊤

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.support, Set.univ, setOf, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
⊢ I ≤ I.radical

Tactic:
fun _ ↦ Ideal.le_radical

Premises used: Set.Mem, Ideal.le_radical
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := X.IdealSheafData) (radical ⊤) ⊤

Tactic:
top_le_iff.mp (le_radical _)

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.le_radical, top_le_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ radical ⊥ = X.nilradical

Tactic:
rfl

Premises used: AlgebraicGeometry.Scheme.nilradical, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
h : ∀ (U : (↑X.affineOpens : Type u)), (I ⊔ J).radical.ideal U = (I.radical ⊔ J.radical).radical.ideal U
⊢ (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

Tactic:
ext U : 2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (I ⊔ J).radical.ideal U = (I.radical ⊔ J.radical).radical.ideal U

Tactic:
(Ideal.radical_sup (I.ideal U) (J.ideal U))

Premises used: Ideal.radical_sup, Set.Mem, setOf, Ideal.radical, AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (I ⊔ J).radical.ideal U = (I.radical ⊔ J.radical).radical.ideal U

Tactic:
exact (Ideal.radical_sup (I.ideal U) (J.ideal U))

Premises used: Ideal.radical_sup, AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
h : ∀ (U : (↑X.affineOpens : Type u)), (I ⊓ J).radical.ideal U = (I.radical ⊓ J.radical).ideal U
⊢ (I ⊓ J).radical = I.radical ⊓ J.radical

Tactic:
ext U : 2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (I ⊓ J).radical.ideal U = (I.radical ⊓ J.radical).ideal U

Tactic:
simp only [radical_ideal, ideal_inf, Pi.inf_apply, Ideal.radical_inf]

Premises used: Ideal.radical_inf, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, Pi.inf_apply
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
h : ∀ (U : (↑X.affineOpens : Type u)), (I * J).radical.ideal U = (I.radical ⊓ J.radical).ideal U
⊢ (I * J).radical = I.radical ⊓ J.radical

Tactic:
ext U : 2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ (I * J).radical.ideal U = (I.radical ⊓ J.radical).ideal U

Tactic:
simp only [radical_ideal, ideal_mul, Pi.mul_apply, Ideal.radical_mul, ideal_inf, Pi.inf_apply]

Premises used: Pi.mul_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal, AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, Pi.inf_apply, Ideal.radical_mul
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
a :
  LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
a₁ :
  LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
a :
  LE.le (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    (Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        (X.affineBasicOpen f)))
⊢ LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))

Tactic:
rw [Ideal.map_le_iff_le_comap]

Premises used: Ideal.map_le_iff_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x
this :
  ∀ (p : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))),
    Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) p : ↥X) →
      Membership.mem (α := (↑Γ(X, X.basicOpen f) : Type u)) p.asIdeal
        ((CommRingCat.Hom.hom F : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) x :
          (↑Γ(X, X.basicOpen f) : Type u))
⊢ Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    (Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        (X.affineBasicOpen f)))
    x

Tactic:
simpa [PrimeSpectrum.mem_vanishingIdeal] using this

Premises used: PrimeSpectrum.mem_vanishingIdeal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x
a :
  ∀ (p : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))),
    Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) p : ↥X) →
      Membership.mem (α := (↑Γ(X, X.basicOpen f) : Type u)) p.asIdeal
        ((CommRingCat.Hom.hom F : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) x :
          (↑Γ(X, X.basicOpen f) : Type u))
⊢ Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    (Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        (X.affineBasicOpen f)))
    x

Tactic:
suffices ∀ p, (X.affineBasicOpen f).2.fromSpec p ∈ Z → F.hom x ∈ p.asIdeal by
          simpa [PrimeSpectrum.mem_vanishingIdeal] using this
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x_1 : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x_1
x : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))
hxZ : Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) x : ↥X)
⊢ Membership.mem (α := (↑Γ(X, X.basicOpen f) : Type u)) x.asIdeal
    ((CommRingCat.Hom.hom F : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) x_1 :
      (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
(PrimeSpectrum.mem_vanishingIdeal _ _).mp hx
          (Spec.map (X.presheaf.map (homOfLE _).op) x) ?_

Premises used: CategoryTheory.ConcreteCategory.hom, Set.Mem, Quiver.Hom.op, setOf, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Set.preimage, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.basicOpen, Iff.mp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, PrimeSpectrum.mem_vanishingIdeal, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x_1 : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x_1
x : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))
hxZ : Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) x : ↥X)
a :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) (γ :=
    Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
    ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens)))))
⊢ Membership.mem (α := (↑Γ(X, X.basicOpen f) : Type u)) x.asIdeal
    ((CommRingCat.Hom.hom F : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) x_1 :
      (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
refine (PrimeSpectrum.mem_vanishingIdeal _ _).mp hx
          (Spec.map (X.presheaf.map (homOfLE _).op) x) ?_

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.homOfLE, Iff.mp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, PrimeSpectrum.mem_vanishingIdeal, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x_1 : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x_1
x : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))
hxZ : Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) x : ↥X)
a :
  Membership.mem (α := ↥X) (↑Z : Set ↥X)
    ((IsAffineOpen.fromSpec ⋯)
        ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens))))) :
      ↥X)
a₁ :
  Membership.mem (α := ↥X) (↑Z : Set ↥X) ((Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ IsAffineOpen.fromSpec ⋯) x : ↥X)
a₂ a₃ a₄ a₅ : Membership.mem (α := ↥X) (↑Z : Set ↥X) ((IsAffineOpen.fromSpec ⋯) x : ↥X)
⊢ Membership.mem (α := PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) (γ :=
    Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
    ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens)))))

Tactic:
rwa [Set.mem_preimage, ← Scheme.Hom.comp_apply,
          IsAffineOpen.map_fromSpec _ (X.affineBasicOpen f).2]

Premises used: AlgebraicGeometry.IsAffineOpen.map_fromSpec, AlgebraicGeometry.Scheme.affineBasicOpen, AlgebraicGeometry.Scheme.Hom.comp_apply, Set.mem_preimage, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
have : IsLocalization.Away f Γ(X, X.basicOpen f) :=
          U.2.isLocalization_of_eq_basicOpen _ _ rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) x
⊢ Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)

Tactic:
have : Topology.IsOpenEmbedding (Spec.map F) :=
          localization_away_isOpenEmbedding Γ(X, X.basicOpen f) f
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) x
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map (X.presheaf.map (homOfLE ⋯).op)))
        (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x

Tactic:
rw [← U.2.map_fromSpec (X.affineBasicOpen f).2 (homOfLE (X.basicOpen_le f)).op,
          Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp] at hx

Premises used: AlgebraicGeometry.IsAffineOpen.map_fromSpec, Quiver.Hom.op, AlgebraicGeometry.Scheme.basicOpen_le, Set.preimage_comp, AlgebraicGeometry.Scheme.affineBasicOpen, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) x
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
hx₁ :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map (X.presheaf.map (homOfLE ⋯).op)))
        (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x
⊢ Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)

Tactic:
rw [← U.2.map_fromSpec (X.affineBasicOpen f).2 (homOfLE (X.basicOpen_le f)).op,
          Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp] at hx

Premises used: AlgebraicGeometry.IsAffineOpen.map_fromSpec, Quiver.Hom.op, AlgebraicGeometry.Scheme.basicOpen_le, Set.preimage_comp, AlgebraicGeometry.Scheme.affineBasicOpen, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map (X.presheaf.map (homOfLE ⋯).op)))
        (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
a :
  ∀ (Z' : Set ↥(Spec Γ(X, (↑U : X.Opens))))
    (hx :
      Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
        (PrimeSpectrum.vanishingIdeal (⇑(Spec.map (X.presheaf.map (homOfLE ⋯).op)) ⁻¹' Z')) x),
    Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')) x
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x

Tactic:
generalize U.2.fromSpec ⁻¹' Z = Z' at hx ⊢

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, (↑U : X.Opens)))
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal (⇑(Spec.map (X.presheaf.map (homOfLE ⋯).op)) ⁻¹' Z')) x
⊢ Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u)) (PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' Z')) x

Tactic:
replace hx : x ∈ vanishingIdeal (Spec.map F ⁻¹' Z') := hx
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, (↑U : X.Opens)))
hx : Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u)) (PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' Z')) x
a :
  ∀ (I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (hI : I.IsRadical)
    (e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))),
    Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')) x
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')) x

Tactic:
obtain ⟨I, hI, e⟩ :=
          (isClosed_iff_zeroLocus_radical_ideal _).mp (isClosed_closure (s := Z'))

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus_radical_ideal, Iff.mp, isClosed_closure