awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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 (γ := 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
have 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
Tactic: erw [preimage_comap_zeroLocus] at hx
Cleared hypotheses: hx, hI, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
      (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
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 (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
have a : ∀
  (hx :
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (PrimeSpectrum.vanishingIdeal
        (PrimeSpectrum.zeroLocus
          (↑(Ideal.span
                ((⇑(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)))) :
            Set (↑Γ(X, X.basicOpen f) : 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 sorry).op))
      (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
Tactic: rwa [← PrimeSpectrum.zeroLocus_span, ← Ideal.map, vanishingIdeal_zeroLocus_eq_radical,
          ← RingHom.algebraMap_toAlgebra (X.presheaf.map _).hom,
          ← IsLocalization.map_radical (.powers f), ← vanishingIdeal_zeroLocus_eq_radical] at hx
Cleared hypotheses: hx, hI, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
      (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
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
a :
  ∀
    (hx :
      Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (PrimeSpectrum.vanishingIdeal
          (PrimeSpectrum.zeroLocus
            (↑(Ideal.span
                  ((⇑(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)))) :
              Set (↑Γ(X, X.basicOpen f) : 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 (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 (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
have a₁ : ∀
  (hx :
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (PrimeSpectrum.vanishingIdeal
        (PrimeSpectrum.zeroLocus (↑(Ideal.map (CommRingCat.Hom.hom F) I) : Set (↑Γ(X, X.basicOpen f) : 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 sorry).op))
      (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
Tactic: rwa [← PrimeSpectrum.zeroLocus_span, ← Ideal.map, vanishingIdeal_zeroLocus_eq_radical,
          ← RingHom.algebraMap_toAlgebra (X.presheaf.map _).hom,
          ← IsLocalization.map_radical (.powers f), ← vanishingIdeal_zeroLocus_eq_radical] at hx
Cleared hypotheses: hx, hI, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 ∈
      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))
have trans : x ∈ (↑Z : Set ↥X) ↔
  x ∈
    X.zeroLocus
        (↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X))) :
          Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩
      (↑(↑U : X.Opens) : Set ↥X)
Tactic: trans x ∈ X.zeroLocus (U := U.1) (vanishingIdeal (U.2.fromSpec ⁻¹' Z)) ∩ U.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ 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))
have trans₁ : x ∈
    X.zeroLocus
        (↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑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 sorry) ⁻¹' (↑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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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 ∈
      X.zeroLocus
          (↑(PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) :
            Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩
        (↑(↑U : X.Opens) : Set ↥X)
have rw : x ∈ (↑Z : Set ↥X) ↔ x ∈ (↑Z : Set ↥X) ∩ (↑(↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ Z ≤ I.support ↔ I ≤ vanishingIdeal Z
have simp : Z ≤ I.support ↔
  ∀ (U : (↑X.affineOpens : Type u)),
    Subset (α := Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: simp only [le_def, vanishingIdeal_ideal, ← PrimeSpectrum.subset_zeroLocus_iff_le_vanishingIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
⊢ 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)))
have 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)
Tactic: trans ∀ U : X.affineOpens, (Z : Set X) ∩ U ⊆ I.support ∩ U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ 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)))
have 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 sorry) ⁻¹' (↑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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
have 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
Tactic: refine ⟨fun H U x hx ↦ ⟨H hx.1, hx.2⟩, fun H x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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
⊢ x ∈ I.support
have obtain : ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)), x ∈ I.support
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)))
have 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 sorry) ⁻¹' (↑Z : Set ↥X))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: refine forall_congr' fun U ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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) ↔
    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)))
have 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 sorry) ⁻¹' (↑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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)))
⊢ (↑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)))
have 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 sorry))
      (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X)))
    (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
      (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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))))
⊢ (↑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)))
have 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 sorry) ⊆
    Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
      (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)))
⊢ (↑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)))
have 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 sorry) ⊆
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
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)
⊢ (↑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)))
have 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)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ vanishingIdeal I.support = I.radical
have h : ∀ (U : (↑X.affineOpens : Type u)), (vanishingIdeal I.support).ideal U = I.radical.ideal U
Tactic: ext U : 2