-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma subset_support_iff_le_vanishingIdeal {I : X.IdealSheafData} {Z : Set X} :
    Z ⊆ I.support ↔ I ≤ vanishingIdeal Z

Proof state:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
H : ∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
hx : x ∈ Z
⊢ x ∈ I.support

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

Result:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
H : ∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
hx : x ∈ Z
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ I.support

Proof state:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
⊢ Z ⊆ I.support ↔
    ∀ (U : ↑X.affineOpens),
      ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
trans ∀ U : X.affineOpens, Z ∩ U ⊆ I.support ∩ U

Result:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
⊢ Z ⊆ I.support ↔ ∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U

X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
⊢ (∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U) ↔
    ∀ (U : ↑X.affineOpens),
      ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Proof state:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
U : ↑X.affineOpens
⊢ Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U ↔
    ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
rw [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]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
H : ∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
hx : x ∈ Z
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ I.support

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

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
⊢ Z ⊆ I.support ↔ ∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U

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

Result:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
H : ∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U
x : ↑↑X.toPresheafedSpace
hx : x ∈ Z
⊢ x ∈ I.support

Proof state:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
⊢ Z ⊆ I.support ↔ I ≤ vanishingIdeal Z

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

Result:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
⊢ Z ⊆ I.support ↔
    ∀ (U : ↑X.affineOpens),
      ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Proof state:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
⊢ (∀ (U : ↑X.affineOpens), Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U) ↔
    ∀ (U : ↑X.affineOpens),
      ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
refine forall_congr' fun U ↦ ?_

Result:
X : Scheme
I : X.IdealSheafData
Z : Set ↑↑X.toPresheafedSpace
U : ↑X.affineOpens
⊢ Z ∩ ↑↑U ⊆ I.support ∩ ↑↑U ↔
    ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' Z ⊆ PrimeSpectrum.zeroLocus ↑(I.ideal U)