-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma Opens.toSpecΓ_preimage_zeroLocus {X : Scheme.{u}} (U : X.Opens)
    (s : Set Γ(X, U)) :
    U.toSpecΓ.base ⁻¹' PrimeSpectrum.zeroLocus s = U.1 ↓∩ X.zeroLocus s

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑(hom (↑U).toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus (⇑(CommRingCat.Hom.hom U.topIso.inv) '' s) =
    U.carrier ↓∩ X.zeroLocus s

Tactic:
rw [Scheme.toSpecΓ_preimage_zeroLocus]

Result:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ (↑U).zeroLocus (⇑(CommRingCat.Hom.hom U.topIso.inv) '' s) = U.carrier ↓∩ X.zeroLocus s

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ (↑U).zeroLocus (⇑(CommRingCat.Hom.hom (U.topIso.inv ≫ (↑U).presheaf.map (eqToHom ⋯).op)) '' s) =
    (↑U).zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)) '' s)

Tactic:
congr!

Result:
case h.e'_3.h.h.e'_5.h.e'_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
a✝¹ : ↑Γ(X, U)
a✝ : a✝¹ ∈ s
⊢ U.topIso.inv ≫ (↑U).presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op

Proof state:
case h.e'_3.h.h.e'_5.h.e'_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
a✝¹ : ↑Γ(X, U)
a✝ : a✝¹ ∈ s
⊢ U.topIso.inv ≫ (↑U).presheaf.map (eqToHom ⋯).op = X.presheaf.map (eqToHom ⋯).op

Tactic:
simp [← Functor.map_comp]

Result:
case h.e'_3.h.h.e'_5.h.e'_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
a✝¹ : ↑Γ(X, U)
a✝ : a✝¹ ∈ s
⊢ X.presheaf.map (eqToHom ⋯ ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) = X.presheaf.map (eqToHom ⋯)

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ (↑U).zeroLocus (⇑(CommRingCat.Hom.hom U.topIso.inv) '' s) = U.carrier ↓∩ X.zeroLocus s

Tactic:
show _ = U.ι.base ⁻¹' (X.zeroLocus s)

Result:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ (↑U).zeroLocus (⇑(CommRingCat.Hom.hom U.topIso.inv) '' s) = ⇑(hom U.ι.base) ⁻¹' X.zeroLocus s

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑(hom U.toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus s = U.carrier ↓∩ X.zeroLocus s

Tactic:
rw [toSpecΓ, Scheme.comp_base, TopCat.coe_comp, Set.preimage_comp, Spec.map_base, hom_ofHom]

Result:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑(hom (↑U).toSpecΓ.base) ⁻¹'
      (⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom U.topIso.inv)) ⁻¹' PrimeSpectrum.zeroLocus s) =
    U.carrier ↓∩ X.zeroLocus s

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑(hom (↑U).toSpecΓ.base) ⁻¹'
      (⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom U.topIso.inv)) ⁻¹' PrimeSpectrum.zeroLocus s) =
    U.carrier ↓∩ X.zeroLocus s

Tactic:
erw [PrimeSpectrum.preimage_comap_zeroLocus]

Result:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ ⇑(hom (↑U).toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus (⇑(CommRingCat.Hom.hom U.topIso.inv) '' s) =
    U.carrier ↓∩ X.zeroLocus s

Proof state:
case h.e'_3.h.h.e'_5.h.e'_3
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
a✝¹ : ↑Γ(X, U)
a✝ : a✝¹ ∈ s
⊢ X.presheaf.map (eqToHom ⋯ ≫ ((Hom.opensFunctor U.ι).map (eqToHom ⋯)).op) = X.presheaf.map (eqToHom ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ (↑U).zeroLocus (⇑(CommRingCat.Hom.hom U.topIso.inv) '' s) = ⇑(hom U.ι.base) ⁻¹' X.zeroLocus s

Tactic:
rw [Scheme.preimage_zeroLocus, U.ι_app_self, ← zeroLocus_map_of_eq _ U.ι_preimage_self,
  ← Set.image_comp, ← RingHom.coe_comp, ← CommRingCat.hom_comp]

Result:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ (↑U).zeroLocus (⇑(CommRingCat.Hom.hom (U.topIso.inv ≫ (↑U).presheaf.map (eqToHom ⋯).op)) '' s) =
    (↑U).zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom ⋯).op)) '' s)