-- Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
lemma isAffine_of_isAffineOpen_basicOpen (s : Set Γ(X, ⊤))
    (hs : Ideal.span s = ⊤) (hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)) :
    IsAffine X

Proof state:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
⊢ IsAffine X

Tactic:
have : CompactSpace X := by
  obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
  rw [← isCompact_univ_iff, ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e]
  simp only [Finset.mem_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk]
  apply s'.isCompact_biUnion
  exact fun i hi ↦ (hs₂ _ (hs' hi)).isCompact

Result:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ IsAffine X

Proof state:
case affine
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ IsIso X.toSpecΓ

Tactic:
refine HasAffineProperty.of_iSup_eq_top (P := MorphismProperty.isomorphisms Scheme)
  (fun i : s ↦ ⟨PrimeSpectrum.basicOpen i.1, ?_⟩) ?_ (fun i ↦ ⟨?_, ?_⟩)

Result:
case affine.refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ PrimeSpectrum.basicOpen ↑i ∈ (Spec Γ(X, ⊤)).affineOpens

case affine.refine_2
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ ⨆ i, ↑((fun i => ⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩) i) = ⊤

case affine.refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsAffine ↑(X.toSpecΓ ⁻¹ᵁ ↑((fun i => ⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩) i))

case affine.refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsIso (Scheme.Hom.appTop (X.toSpecΓ ∣_ ↑((fun i => ⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩) i)))

Proof state:
case affine.refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsAffine ↑(X.toSpecΓ ⁻¹ᵁ ↑((fun i => ⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩) i))

Tactic:
rw [Scheme.toSpecΓ_preimage_basicOpen]

Result:
case affine.refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsAffine ↑(X.basicOpen ↑i)

Proof state:
case affine.refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ PrimeSpectrum.basicOpen ↑i ∈ (Spec Γ(X, ⊤)).affineOpens

Tactic:
show IsAffineOpen _

Result:
case affine.refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsAffineOpen (PrimeSpectrum.basicOpen ↑i)

Proof state:
case intro.intro
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ ∀ i ∈ s', IsCompact ↑(X.basicOpen i)

Tactic:
exact fun i hi ↦ (hs₂ _ (hs' hi)).isCompact

Result:
no goals

Proof state:
case affine.refine_3
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsAffine ↑(X.basicOpen ↑i)

Tactic:
exact hs₂ _ i.2

Result:
no goals

Proof state:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ IsAffine X

Tactic:
constructor

Result:
case affine
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ IsIso X.toSpecΓ

Proof state:
case affine.refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsAffineOpen (PrimeSpectrum.basicOpen ↑i)

Tactic:
simp only [← basicOpen_eq_of_affine]

Result:
case affine.refine_1
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsAffineOpen ((Spec Γ(X, ⊤)).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, ⊤)).inv) ↑i))

Proof state:
case intro.intro
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact ↑(⨆ i ∈ ↑s', X.basicOpen i)

Tactic:
simp only [Finset.mem_coe, Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk]

Result:
case intro.intro
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact (⋃ i ∈ s', ↑(X.basicOpen i))

Proof state:
case intro.intro
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ IsCompact (⋃ i ∈ s', ↑(X.basicOpen i))

Tactic:
apply s'.isCompact_biUnion

Result:
case intro.intro
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
s' : Finset ↑Γ(X, ⊤)
hs' : ↑s' ⊆ s
e : Ideal.span ↑s' = ⊤
⊢ ∀ i ∈ s', IsCompact ↑(X.basicOpen i)

Proof state:
case affine.refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsIso (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen ↑i) ''ᵁ ⊤) ≫ X.presheaf.map (eqToHom ⋯).op)

Tactic:
refine IsIso.comp_isIso' ?_ inferInstance

Result:
case affine.refine_4
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace
this : CompactSpace ↑↑X.toPresheafedSpace
i : ↑s
⊢ IsIso (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen ↑i) ''ᵁ ⊤))