-- 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:
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)))

Tactic:
simp only [Functor.comp_obj, Functor.rightOp_obj, Scheme.Γ_obj, Scheme.Spec_obj, id_eq,
  eq_mpr_eq_cast, Functor.id_obj, Opens.map_top, morphismRestrict_app]

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) ''ᵁ ⊤) ≫ X.presheaf.map (eqToHom ⋯).op)

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) ''ᵁ ⊤))

Tactic:
convert isIso_ΓSpec_adjunction_unit_app_basicOpen i.1 using 0

Result:
case a
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) ''ᵁ ⊤)) ↔
    IsIso ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen ↑i)))

Proof state:
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) = ⊤

Tactic:
rw [PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq, hs]

Result:
no goals

Proof state:
case a
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
⊢ Scheme.Opens.ι (PrimeSpectrum.basicOpen ↑i) ''ᵁ ⊤ = PrimeSpectrum.basicOpen ↑i

Tactic:
rw [Opens.isOpenEmbedding_obj_top]

Result:
no goals

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' = ⊤
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
rw [← isCompact_univ_iff, ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e]

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 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))

Tactic:
exact (isAffineOpen_top (Scheme.Spec.obj (op _))).basicOpen _

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
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp hs

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' = ⊤
⊢ CompactSpace ↑↑X.toPresheafedSpace

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

Tactic:
have : QuasiSeparatedSpace X := isAffineOpen_of_isAffineOpen_basicOpen_aux s hs hs₂

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

Proof state:
case a
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) ''ᵁ ⊤)) ↔
    IsIso ((ΓSpec.adjunction.unit.app X).c.app (op (PrimeSpectrum.basicOpen ↑i)))

Tactic:
refine congr(IsIso ((ΓSpec.adjunction.unit.app X).app $(?_)))

Result:
case a
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
⊢ Scheme.Opens.ι (PrimeSpectrum.basicOpen ↑i) ''ᵁ ⊤ = PrimeSpectrum.basicOpen ↑i