-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem basicOpen_union_eq_self_iff (s : Set Γ(X, U)) :
    ⨆ f : s, X.basicOpen (f : Γ(X, U)) = U ↔ Ideal.span s = ⊤

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ ↔ Ideal.span s = ⊤

Tactic:
simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.zeroLocus {↑i})ᶜ = Set.univ ↔ Ideal.span s = ⊤

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : (⨆ f, X.basicOpen ↑f).carrier ∩ ↑U = U.carrier ∩ ↑U
⊢ ⨆ f, X.basicOpen ↑f = U

Tactic:
simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ⨆ f, X.basicOpen ↑f = U

Proof state:
case a.h.e'_2.h.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↑↑(Spec Γ(X, U)).toPresheafedSpace = Set (PrimeSpectrum ↑Γ(X, U))
x : ↑s
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen ↑x) = (PrimeSpectrum.basicOpen ↑x).carrier

Tactic:
exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ↑(⨆ f, X.basicOpen ↑f) = ↑U

Tactic:
refine Set.Subset.antisymm ?_ h

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.zeroLocus {↑i})ᶜ = Set.univ ↔ Ideal.span s = ⊤

Tactic:
rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
  PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus s = ∅

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑U

Tactic:
simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ∀ x ∈ s, ↑(X.basicOpen x) ⊆ ↑U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen ↑i) =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
congr! 1

Result:
case a.h.e'_2.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↑↑(Spec Γ(X, U)).toPresheafedSpace = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⋃ i, ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen ↑i) = ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier

case a.h.e'_3.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↑↑(Spec Γ(X, U)).toPresheafedSpace = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier = Set.univ

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h :
  ⇑(ConcreteCategory.hom hU.fromSpec.base) ''
      (⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier) =
    ⇑(ConcreteCategory.hom hU.fromSpec.base) '' (⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier)
⊢ ⨆ f, X.basicOpen ↑f = U

Tactic:
rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.range_fromSpec]
  at h

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : (⨆ f, X.basicOpen ↑f).carrier ∩ ↑U = U.carrier ∩ ↑U
⊢ ⨆ f, X.basicOpen ↑f = U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ Ideal.span s = ⊤

Tactic:
trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ ↔ Ideal.span s = ⊤

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔
    ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier

Tactic:
refine ⟨fun h => by rw [h], ?_⟩

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier →
    ⨆ f, X.basicOpen ↑f = U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ⨆ f, X.basicOpen ↑f = U
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
    ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier

Tactic:
rw [h]

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier →
    ⨆ f, X.basicOpen ↑f = U

Tactic:
intro h

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h :
  ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
    ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier
⊢ ⨆ f, X.basicOpen ↑f = U

Proof state:
case a.h.e'_2.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↑↑(Spec Γ(X, U)).toPresheafedSpace = Set (PrimeSpectrum ↑Γ(X, U))
⊢ (fun i => ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen ↑i)) = fun i =>
    (PrimeSpectrum.basicOpen ↑i).carrier

Tactic:
ext1 x

Result:
case a.h.e'_2.h.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↑↑(Spec Γ(X, U)).toPresheafedSpace = Set (PrimeSpectrum ↑Γ(X, U))
x : ↑s
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen ↑x) = (PrimeSpectrum.basicOpen ↑x).carrier

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion]

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⋃ i, ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' ↑(X.basicOpen ↑i) =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔ ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
trans
  hU.fromSpec.base ⁻¹' (⨆ f : s, X.basicOpen (f : Γ(X, U))).1 =
    hU.fromSpec.base ⁻¹' U.1

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⨆ f, X.basicOpen ↑f = U ↔
    ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier

X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
      ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Proof state:
case a.h.e'_3.h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
e_1✝ : Set ↑↑(Spec Γ(X, U)).toPresheafedSpace = Set (PrimeSpectrum ↑Γ(X, U))
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier = Set.univ

Tactic:
exact congr_arg Opens.carrier hU.fromSpec_preimage_self

Result:
no goals