-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
/-- On a locally ringed space `X`, the preimage of the zero locus of the prime spectrum
of `Γ(X, ⊤)` under `toΓSpec` agrees with the associated zero locus on `X`. -/
lemma toΓSpec_preimage_zeroLocus_eq {X : LocallyRingedSpace.{u}}
    (s : Set (X.presheaf.obj (op ⊤))) :
    X.toΓSpec.base ⁻¹' PrimeSpectrum.zeroLocus s = X.toRingedSpace.zeroLocus s

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⋂ i ∈ s, ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ

Tactic:
simp_rw [← Set.preimage_iInter₂, Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl,
  compl_compl]

Result:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, zeroLocus {i}

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Tactic:
rw [Set.preimage_compl, Opens.carrier_eq_coe]

Result:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ↑(basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ

Tactic:
symm

Result:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus (⋃ i ∈ s, {i})

Tactic:
simp

Result:
no goals

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ⋂ i ∈ s, zeroLocus {i}

Tactic:
rw [← PrimeSpectrum.zeroLocus_iUnion₂]

Result:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus (⋃ i ∈ s, {i})

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = X.toRingedSpace.zeroLocus s

Tactic:
simp only [RingedSpace.zeroLocus]

Result:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ

Tactic:
erw [Set.iInter₂_congr this]

Result:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⋂ i ∈ s, ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ

Tactic:
have (i : LocallyRingedSpace.Γ.obj (op X)) (_ : i ∈ s) :
    (SetLike.coe (X.toRingedSpace.basicOpen i))ᶜ =
      X.toΓSpec.base ⁻¹' ((PrimeSpectrum.basicOpen i).carrier)ᶜ := by
  symm
  rw [Set.preimage_compl, Opens.carrier_eq_coe]
  erw [X.toΓSpec_preimage_basicOpen_eq i]

Result:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s = ⋂ f ∈ s, (↑(X.toRingedSpace.basicOpen f))ᶜ

Proof state:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ↑(basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Tactic:
erw [X.toΓSpec_preimage_basicOpen_eq i]

Result:
no goals