-- Mathlib/AlgebraicGeometry/AffineScheme.lean
/--
Given a spanning set of `Γ(X, U)`, the corresponding basic open sets cover `U`.
See `IsAffineOpen.basicOpen_union_eq_self_iff` for the inverse direction for affine open sets.
-/
lemma iSup_basicOpen_of_span_eq_top {X : Scheme} (U) (s : Set Γ(X, U))
    (hs : Ideal.span s = ⊤) : (⨆ i ∈ s, X.basicOpen i) = U

Proof state:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := (isBasis_affine_open X).exists_subset_of_mem_open hx U.2

Result:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ x ∈ ↑(⨆ i ∈ s, X.basicOpen i)

Proof state:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ x ∈ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
refine SetLike.mem_of_subset ?_ hxV

Result:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑V ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Proof state:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ U ≤ ⨆ i ∈ s, X.basicOpen i

Tactic:
intro x hx

Result:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
⊢ x ∈ ↑(⨆ i ∈ s, X.basicOpen i)

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ⨆ i ∈ s, X.basicOpen i = U

Tactic:
apply le_antisymm

Result:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ⨆ i ∈ s, X.basicOpen i ≤ U

case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ U ≤ ⨆ i ∈ s, X.basicOpen i

Proof state:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ∀ i ∈ s, X.basicOpen i ≤ U

Tactic:
exact fun i _ ↦ X.basicOpen_le i

Result:
no goals

Proof state:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ∀ i ∈ s, ↑V ∩ ↑(X.basicOpen i) ⊆ ⋃ i ∈ s, ↑(X.basicOpen i)

Tactic:
exact fun i hi ↦ (Set.inter_subset_right.trans
  (Set.subset_iUnion₂ (s := fun x _ ↦ (X.basicOpen x : Set X)) i hi))

Result:
no goals

Proof state:
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ Ideal.span (⇑(ConcreteCategory.hom (X.presheaf.map (homOfLE hVU).op)) '' s) = ⊤

Tactic:
rw [← Ideal.map_span, hs, Ideal.map_top]

Result:
no goals

Proof state:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑V ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
rw [← (hV.basicOpen_union_eq_self_iff (X.presheaf.map (homOfLE hVU).op '' s)).mpr
  (by rw [← Ideal.map_span, hs, Ideal.map_top])]

Result:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Proof state:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ↑(⨆ f, X.basicOpen ↑f) ⊆ ↑(⨆ i ∈ s, X.basicOpen i)

Tactic:
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image,
  Set.iUnion_exists, Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res,
  Opens.coe_inf, Opens.coe_mk, Set.iUnion_subset_iff]

Result:
case a.intro.intro.intro.intro.intro
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑U
V : Opens ↑↑X.toPresheafedSpace
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ↑U
⊢ ∀ i ∈ s, ↑V ∩ ↑(X.basicOpen i) ⊆ ⋃ i ∈ s, ↑(X.basicOpen i)

Proof state:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ⨆ i ∈ s, X.basicOpen i ≤ U

Tactic:
rw [iSup₂_le_iff]

Result:
case a
X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
hs : Ideal.span s = ⊤
⊢ ∀ i ∈ s, X.basicOpen i ≤ U