-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem of_affine_open_cover {X : Scheme} {P : X.affineOpens → Prop}
    {ι} (U : ι → X.affineOpens) (iSup_U : (⨆ i, U i : X.Opens) = ⊤)
    (V : X.affineOpens)
    (basicOpen : ∀ (U : X.affineOpens) (f : Γ(X, U)), P U → P (X.affineBasicOpen f))
    (openCover :
      ∀ (U : X.affineOpens) (s : Finset (Γ(X, U)))
        (_ : Ideal.span (s : Set (Γ(X, U))) = ⊤),
        (∀ f : s, P (X.affineBasicOpen f.1)) → P U)
    (hU : ∀ i, P (U i)) : P V

Proof state:
case intro.intro.mk
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
this : Ideal.span (Set.range f) = ⊤
t : Finset ↑Γ(X, ↑V)
ht₁ : ↑t ⊆ Set.range f
ht₂ : Ideal.span ↑t = ⊤
i : ↑Γ(X, ↑V)
hi : i ∈ t
⊢ P (X.affineBasicOpen ↑⟨i, hi⟩)

Tactic:
obtain ⟨x, rfl⟩ := ht₁ hi

Result:
case intro.intro.mk.intro
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
this : Ideal.span (Set.range f) = ⊤
t : Finset ↑Γ(X, ↑V)
ht₁ : ↑t ⊆ Set.range f
ht₂ : Ideal.span ↑t = ⊤
x : ↥↑V
hi : f x ∈ t
⊢ P (X.affineBasicOpen ↑⟨f x, hi⟩)

Proof state:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ ↑V ≤ ⨆ f_1, X.basicOpen ↑f_1

Tactic:
intro x hx

Result:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↑↑X.toPresheafedSpace
hx : x ∈ ↑↑V
⊢ x ∈ ↑(⨆ f_1, X.basicOpen ↑f_1)

Proof state:
case h.e'_1
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ X.affineBasicOpen f = X.affineBasicOpen g

Tactic:
ext1

Result:
case h.e'_1.a
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ ↑(X.affineBasicOpen f) = ↑(X.affineBasicOpen g)

Proof state:
case h.e'_1.a
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
f : ↑Γ(X, ↑V)
g : ↑Γ(X, ↑(U i))
e : X.basicOpen f = X.basicOpen g
hf : ↑x ∈ X.basicOpen f
⊢ ↑(X.affineBasicOpen f) = ↑(X.affineBasicOpen g)

Tactic:
exact e

Result:
no goals

Proof state:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
this : ∀ (x : ↥↑V), ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
⊢ P V

Tactic:
choose f hf₁ hf₂ using this

Result:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
⊢ P V

Proof state:
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (show x.1 ∈ (⨆ i, U i : X.Opens) from iSup_U ▸ trivial)

Result:
case intro
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
x : ↥↑V
i : ι
hi : ↑x ∈ ↑(U i)
⊢ ∃ f, ↑x ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Proof state:
case intro.intro.mk.intro
X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)),
    Ideal.span ↑s = ⊤ → (∀ (f : { x // x ∈ s }), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
this : Ideal.span (Set.range f) = ⊤
t : Finset ↑Γ(X, ↑V)
ht₁ : ↑t ⊆ Set.range f
ht₂ : Ideal.span ↑t = ⊤
x : ↥↑V
hi : f x ∈ t
⊢ P (X.affineBasicOpen ↑⟨f x, hi⟩)

Tactic:
exact hf₂ x

Result:
no goals