-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma zeroLocus_inter_subset_support (I : IdealSheafData X) (U : X.affineOpens) :
    X.zeroLocus (U := U.1) (I.ideal U) ∩ U ⊆ I.support

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
⊢ False

Tactic:
have inst := U.2.isLocalization_basicOpen f

Result:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ False

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
⊢ False

Tactic:
obtain ⟨⟨s', ⟨_, n, rfl⟩⟩, hs'⟩ :=
  (IsLocalization.mem_map_algebraMap_iff (.powers f) Γ(X, X.basicOpen f)).mp this

Result:
case intro.intro.intro.intro.intro.intro.mk.mk.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
      (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).2 =
    (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).1
⊢ False

Proof state:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊆ X.zeroLocus ↑(I.ideal V)

Tactic:
apply (X.codisjoint_zeroLocus (U := V) (I.ideal V)).symm.left_le_of_le_inf_right

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊓ ↑↑V ≤ X.zeroLocus ↑(I.ideal V)

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊆ I.support

Tactic:
refine Set.subset_iInter fun V ↦ ?_

Result:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊆ X.zeroLocus ↑(I.ideal V)

Proof state:
case intro.intro.intro.intro.intro.intro.mk.mk.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).1))
⊢ False

Tactic:
refine hx s' s'.2 ?_

Result:
case intro.intro.intro.intro.intro.intro.mk.mk.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x => f ^ x) n, ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈ I.ideal (X.affineBasicOpen f)
⊢ False

Tactic:
rw [← I.map_ideal_basicOpen] at this

Result:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
⊢ False

Proof state:
case intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hx : x ∈ X.zeroLocus ↑(I.ideal U)
hxU : x ∈ ↑↑U
⊢ x ∈ X.zeroLocus ↑(I.ideal V)

Tactic:
simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe] at hx ⊢

Result:
case intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
⊢ ∀ f ∈ I.ideal V, x ∉ X.basicOpen f

Proof state:
case intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
⊢ ∀ f ∈ I.ideal V, x ∉ X.basicOpen f

Tactic:
intro s hfU hxs

Result:
case intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
⊢ False

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ False

Tactic:
have := (I.map_ideal (U := X.affineBasicOpen f) (hfg.trans_le (X.basicOpen_le g))).le
  (Ideal.mem_map_of_mem _ hfU)

Result:
case intro.intro.intro.intro.intro
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↑↑X.toPresheafedSpace
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this : (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈ I.ideal (X.affineBasicOpen f)
⊢ False