awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : 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
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
a :
  ∀ (I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (hx :
      Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (PrimeSpectrum.vanishingIdeal
          (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map F))
            (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
        x)
    (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:
rw [← vanishingIdeal_closure,
          ← this.isOpenMap.preimage_closure_eq_closure_preimage this.continuous, e] at hx

Premises used: Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.preimage_closure_eq_closure_preimage, Topology.IsOpenEmbedding.continuous, PrimeSpectrum.vanishingIdeal_closure
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : 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)))
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map F))
        (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
a :
  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 (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    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:
rw [← vanishingIdeal_closure, e]

Premises used: PrimeSpectrum.vanishingIdeal_closure
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : 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)))
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map F))
        (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (PrimeSpectrum.zeroLocus
        ((⇑(CommRingCat.Hom.hom F) : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) ''
          (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x

Tactic:
erw [preimage_comap_zeroLocus] at hx

Premises used: PrimeSpectrum.preimage_comap_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : 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)))
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map F))
        (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
hx₁ :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (PrimeSpectrum.zeroLocus
        ((⇑(CommRingCat.Hom.hom F) : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) ''
          (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
⊢ I.IsRadical

Tactic:
erw [preimage_comap_zeroLocus] at hx

Premises used: PrimeSpectrum.preimage_comap_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I_1 : 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)))
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map F))
        (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
hx₁ :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (PrimeSpectrum.zeroLocus
        ((⇑(CommRingCat.Hom.hom F) : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) ''
          (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
hI₁ : I.IsRadical
⊢ closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
erw [preimage_comap_zeroLocus] at hx

Premises used: PrimeSpectrum.preimage_comap_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
trans :
  x ∈ (↑Z : Set ↥X) ↔
    x ∈
      X.zeroLocus
          (↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) :
            Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩
        (↑(↑U : X.Opens) : Set ↥X)
trans₁ :
  x ∈
      X.zeroLocus
          (↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) :
            Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩
        (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈
      X.zeroLocus
        (↑((fun (U : (↑X.affineOpens : Type u)) ↦
                (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
                  Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
              U) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ x ∈ (↑Z : Set ↥X) ↔
    x ∈
      X.zeroLocus
        (↑((fun (U : (↑X.affineOpens : Type u)) ↦
                (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
                  Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
              U) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
trans x ∈ X.zeroLocus (U := U.1) (vanishingIdeal (U.2.fromSpec ⁻¹' Z)) ∩ U.1

Premises used: Subtype.val
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
rw : x ∈ (↑Z : Set ↥X) ↔ x ∈ (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ x ∈ (↑Z : Set ↥X) ↔
    x ∈
      X.zeroLocus
          (↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) :
            Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩
        (↑(↑U : X.Opens) : Set ↥X)

Tactic:
rw [← U.2.fromSpec_image_zeroLocus, zeroLocus_vanishingIdeal_eq_closure,
          ← U.2.fromSpec.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage
            U.2.fromSpec.continuous,
          Set.image_preimage_eq_inter_range, Z.isClosed.closure_eq, IsAffineOpen.range_fromSpec]

Premises used: TopologicalSpace.Closeds.isClosed, Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.preimage_closure_eq_closure_preimage, IsClosed.closure_eq, AlgebraicGeometry.IsAffineOpen.fromSpec, Set.image_preimage_eq_inter_range, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈ (↑Z : Set ↥X) ↔ x ∈ (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
simp [hxU]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈
      X.zeroLocus
          (↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) :
            Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩
        (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈
      X.zeroLocus
        (↑((fun (U : (↑X.affineOpens : Type u)) ↦
                (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
                  Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
              U) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u))

Tactic:
simp [hxU]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
simp :
  Z ≤ I.support ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ Z ≤ I.support ↔ I ≤ vanishingIdeal Z

Tactic:
simp only [le_def, vanishingIdeal_ideal, ← PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal, PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, AlgebraicGeometry.Scheme.IdealSheafData.le_def
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
trans :
  Z ≤ I.support ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)
trans₁ :
  (∀ (U : (↑X.affineOpens : Type u)),
      (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)) ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ Z ≤ I.support ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
trans ∀ U : X.affineOpens, (Z : Set X) ∩ U ⊆ I.support ∩ U
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ Z ≤ I.support ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
⟨fun H U x hx ↦ ⟨H hx.1, hx.2⟩, fun H x hx ↦ ?_⟩

Premises used: And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
refine :
  ∀
    (H :
      ∀ (U : (↑X.affineOpens : Type u)),
        (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X))
    (x : ↥X) (hx : x ∈ Z), x ∈ I.support
⊢ Z ≤ I.support ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
refine ⟨fun H U x hx ↦ ⟨H hx.1, hx.2⟩, fun H x hx ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
H :
  ∀ (U : (↑X.affineOpens : Type u)),
    (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)
x : ↥X
hx : x ∈ Z
obtain : ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)), x ∈ I.support
⊢ x ∈ I.support

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

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
H :
  ∀ (U : (↑X.affineOpens : Type u)),
    (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)
x : ↥X
hx : x ∈ Z
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
⊢ x ∈ I.support

Tactic:
(H ⟨U, hU⟩ ⟨hx, hxU⟩).1

Premises used: Subtype.mk, And.left, And.intro
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
H :
  ∀ (U : (↑X.affineOpens : Type u)),
    (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)
x : ↥X
hx : x ∈ Z
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
⊢ x ∈ I.support

Tactic:
exact (H ⟨U, hU⟩ ⟨hx, hxU⟩).1

Premises used: Subtype.mk, And.left, And.intro
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ (∀ (U : (↑X.affineOpens : Type u)),
      (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)) ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
forall_congr' fun U ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
refine :
  ∀ (U : (↑X.affineOpens : Type u)),
    (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
      Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ (∀ (U : (↑X.affineOpens : Type u)),
      (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X)) ↔
    ∀ (U : (↑X.affineOpens : Type u)),
      Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
refine forall_congr' fun U ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
rw :
  (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
rw₁ :
  (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    Subset (α := Set ↥X)
      (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
        (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)))
      (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))
rw₂ :
  (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    (↑Z : Set ↥X) ∩ Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯) ⊆
      Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
        (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
rw₃ :
  (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    (↑Z : Set ↥X) ∩ Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯) ⊆
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
rw₄ rw₅ :
  (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ (↑Z : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
rw [coe_support_inter, ← Set.image_subset_image_iff U.2.fromSpec.isOpenEmbedding.injective,
    Set.image_preimage_eq_inter_range, IsAffineOpen.fromSpec_image_zeroLocus,
    IsAffineOpen.range_fromSpec]

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.IsAffineOpen.fromSpec, Set.image_preimage_eq_inter_range, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Set.image_subset_image_iff, Topology.IsEmbedding.injective, AlgebraicGeometry.IsAffineOpen.range_fromSpec, AlgebraicGeometry.Scheme.IdealSheafData.coe_support_inter, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ GaloisConnection (fun (x : X.IdealSheafData) ↦ x.support) fun (x : (Closeds ↥X)ᵒᵈ) ↦ vanishingIdeal x

Tactic:
fun _ _ ↦ le_support_iff_le_vanishingIdeal

Premises used: Set.Mem, AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal, GaloisConnection
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
S T : Closeds ↥X
h : S ≤ T
⊢ vanishingIdeal T ≤ vanishingIdeal S

Tactic:
gc.monotone_u h

Premises used: GaloisConnection.monotone_u, AlgebraicGeometry.Scheme.IdealSheafData.gc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
h : ∀ (U : (↑X.affineOpens : Type u)), (vanishingIdeal I.support).ideal U = I.radical.ideal U
⊢ vanishingIdeal I.support = I.radical

Tactic:
ext U : 2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
h :
  PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X)) =
    PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X)) = (I.ideal U).radical

Tactic:
rw [← vanishingIdeal_zeroLocus_eq_radical]

Premises used: PrimeSpectrum.vanishingIdeal_zeroLocus_eq_radical
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
h :
  Eq (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X))
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X)) =
    PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
h :
  Eq (α := Set ↥X)
    (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X)))
    (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))
⊢ Eq (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑I.support : Set ↥X))
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
apply U.2.fromSpec.isOpenEmbedding.injective.image_injective

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsEmbedding.injective, Function.Injective.image_injective, Subtype.property