-- Mathlib/AlgebraicGeometry/AffineScheme.lean
/-- If `X` is an affine scheme, every closed set of `X` is the zero locus
of a set of global sections. -/
lemma eq_zeroLocus_of_isClosed_of_isAffine [IsAffine X] (s : Set X) :
    IsClosed s ↔ ∃ I : Ideal (Γ(X, ⊤)), s = X.zeroLocus (I : Set Γ(X, ⊤))

Proof state:
case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
⊢ ∃ I, s = X.zeroLocus ↑I

Tactic:
obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ

Result:
case refine_1.intro
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ ∃ I, s = X.zeroLocus ↑I

Proof state:
case refine_2.intro
X : Scheme
inst✝ : IsAffine X
I : Ideal ↑Γ(X, ⊤)
⊢ IsClosed (X.zeroLocus ↑I)

Tactic:
exact zeroLocus_isClosed X I.carrier

Result:
no goals

Proof state:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ ⇑(hom X.toSpecΓ.base) ⁻¹' (X.toΓSpecFun '' s) = s

Tactic:
exact Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.base).injective

Result:
no goals

Proof state:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ s = X.zeroLocus ↑I

Tactic:
simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]

Result:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ s = ⇑(hom X.toSpecΓ.base) ⁻¹' (X.toΓSpecFun '' s)

Proof state:
case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
⊢ ∃ I, s = X.zeroLocus ↑I

Tactic:
have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs

Result:
case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
⊢ ∃ I, s = X.zeroLocus ↑I

Proof state:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ s = ⇑(hom X.toSpecΓ.base) ⁻¹' (X.toΓSpecFun '' s)

Tactic:
symm

Result:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ ⇑(hom X.toSpecΓ.base) ⁻¹' (X.toΓSpecFun '' s) = s

Proof state:
case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
⊢ ∃ I, s = X.zeroLocus ↑I

Tactic:
let Z : Set (Spec <| Γ(X, ⊤)) := X.toΓSpecFun '' s

Result:
case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
⊢ ∃ I, s = X.zeroLocus ↑I

Proof state:
case refine_2
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
⊢ (∃ I, s = X.zeroLocus ↑I) → IsClosed s

Tactic:
rintro ⟨I, rfl⟩

Result:
case refine_2.intro
X : Scheme
inst✝ : IsAffine X
I : Ideal ↑Γ(X, ⊤)
⊢ IsClosed (X.zeroLocus ↑I)

Proof state:
case refine_1.intro
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ ∃ I, s = X.zeroLocus ↑I

Tactic:
use I

Result:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
Z : Set ↑↑(Spec Γ(X, ⊤)).toPresheafedSpace := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal ↑Γ(X, ⊤)
hI : Z = PrimeSpectrum.zeroLocus ↑I
⊢ s = X.zeroLocus ↑I

Proof state:
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
⊢ IsClosed s ↔ ∃ I, s = X.zeroLocus ↑I

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩

Result:
case refine_1
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
hs : IsClosed s
⊢ ∃ I, s = X.zeroLocus ↑I

case refine_2
X : Scheme
inst✝ : IsAffine X
s : Set ↑↑X.toPresheafedSpace
⊢ (∃ I, s = X.zeroLocus ↑I) → IsClosed s