awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact
    (↑(X.basicOpen (U := (↑V : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑V : X.Opens)))
                (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u))
            (↑i : (↑Γ(X, ⊤) : Type u)))) :
      Set ↥X)

Tactic:
(V.2.basicOpen _).isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.IsAffineOpen.basicOpen, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact
    (↑(X.basicOpen (U := (↑V : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑V : X.Opens)))
                (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u))
            (↑i : (↑Γ(X, ⊤) : Type u)))) :
      Set ↥X)

Tactic:
exact (V.2.basicOpen _).isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.IsAffineOpen.basicOpen, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
have : QuasiSeparatedSpace X := isAffine_of_isAffineOpen_basicOpen_aux s hs hs₂
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
obtain :
  ∀ (s' : Finset (↑Γ(X, ⊤) : Type u)) (hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s)
    (e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤), CompactSpace.{u} ↥X
⊢ CompactSpace.{u} ↥X

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

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
rw : IsCompact (↑(⨆ i ∈ (↑s' : Set (↑Γ(X, ⊤) : Type u)), X.basicOpen i) : Set ↥X)
⊢ CompactSpace.{u} ↥X

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

Premises used: AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, isCompact_univ_iff, TopologicalSpace.Opens.coe_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
simp : IsCompact.{u} (X := ↥X) (⋃ i ∈ s', (↑(X.basicOpen i) : Set ↥X))
⊢ IsCompact (↑(⨆ i ∈ (↑s' : Set (↑Γ(X, ⊤) : Type u)), X.basicOpen i) : Set ↥X)

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

Premises used: TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe, Finset.mem_coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
apply : ∀ i ∈ s', IsCompact (↑(X.basicOpen i) : Set ↥X)
⊢ IsCompact.{u} (X := ↥X) (⋃ i ∈ s', (↑(X.basicOpen i) : Set ↥X))

Tactic:
apply s'.isCompact_biUnion

Premises used: Finset.isCompact_biUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
⊢ ∀ i ∈ s', IsCompact (↑(X.basicOpen i) : Set ↥X)

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

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
⊢ ∀ i ∈ s', IsCompact (↑(X.basicOpen i) : Set ↥X)

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

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace.{u} ↥X
⊢ CompactSpace.{u} ↥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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine : IsIso X.toSpecΓ
⊢ IsAffine X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
⊢ IsIso X.toSpecΓ

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

Premises used: PrimeSpectrum.basicOpen, AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top, Subtype.mk, And.intro, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine :
  ∀ (i : (↑s : Type u)),
    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens
      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))
affine₁ :
  Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
    (⨆ (i : (↑s : Type u)),
      (↑((fun (i : (↑s : Type u)) ↦
              (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                  (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                { x : (Spec Γ(X, ⊤)).Opens //
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
            i) :
        (Spec Γ(X, ⊤)).Opens))
    ⊤
affine₂ :
  ∀ (i : (↑s : Type u)),
    IsAffine.{u}
      (↑(X.toSpecΓ ⁻¹ᵁ
            (↑((fun (i : (↑s : Type u)) ↦
                    (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                        (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                      { x : (Spec Γ(X, ⊤)).Opens //
                        Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
                  i) :
              (Spec Γ(X, ⊤)).Opens)) :
        Scheme)
affine₃ :
  ∀ (i : (↑s : Type u)),
    IsIso (X :=
      Γ((↑(↑((fun (i : (↑s : Type u)) ↦ ⟨PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)), ⋯⟩) i) :
              (Spec Γ(X, ⊤)).Opens) :
          Scheme),
        ⊤))
      (Scheme.Hom.appTop
        (X.toSpecΓ ∣_
          (↑((fun (i : (↑s : Type u)) ↦
                  (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                    { x : (Spec Γ(X, ⊤)).Opens //
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
                i) :
            (Spec Γ(X, ⊤)).Opens)))
⊢ IsIso X.toSpecΓ

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

Premises used: AlgebraicGeometry.HasAffineProperty.of_iSup_eq_top, Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
affine :
  IsAffineOpen.{u} (X := Spec Γ(X, ⊤))
    ((Spec Γ(X, ⊤)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (Scheme.ΓSpecIso Γ(X, ⊤))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
        (↑i : (↑Γ(X, ⊤) : Type u))))
⊢ IsAffineOpen.{u} (X := Spec Γ(X, ⊤)) (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))

Tactic:
simp only [← basicOpen_eq_of_affine]

Premises used: AlgebraicGeometry.basicOpen_eq_of_affine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsAffineOpen.{u} (X := Spec Γ(X, ⊤))
    ((Spec Γ(X, ⊤)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (Scheme.ΓSpecIso Γ(X, ⊤))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
        (↑i : (↑Γ(X, ⊤) : Type u))))

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

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Spec, AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.Scheme.Spec, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsAffineOpen.{u} (X := Spec Γ(X, ⊤))
    ((Spec Γ(X, ⊤)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Iso.inv (Scheme.ΓSpecIso Γ(X, ⊤))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(Spec Γ(X, ⊤), ⊤) : Type u))
        (↑i : (↑Γ(X, ⊤) : Type u))))

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

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.Scheme.Spec, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
affine :
  Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span (Set.range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : (↑Γ(X, ⊤) : Type u)) ↦ x ∈ s)))) ⊤
affine₁ : Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span {x : (↑Γ(X, ⊤) : Type u) | x ∈ s}) ⊤
affine₂ : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
affine₃ affine₄ : Eq.{u + 1} (α := Ideal (↑Γ(X, ⊤) : Type u)) ⊤ ⊤
⊢ Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens)
    (⨆ (i : (↑s : Type u)),
      (↑((fun (i : (↑s : Type u)) ↦
              (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                  (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                { x : (Spec Γ(X, ⊤)).Opens //
                  Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
            i) :
        (Spec Γ(X, ⊤)).Opens))
    ⊤

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

Premises used: PrimeSpectrum.iSup_basicOpen_eq_top_iff, Subtype.range_coe_subtype, Set.setOf_mem_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
affine : IsAffine.{u} (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme)
⊢ IsAffine.{u}
    (↑(X.toSpecΓ ⁻¹ᵁ
          (↑((fun (i : (↑s : Type u)) ↦
                  (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                      (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                    { x : (Spec Γ(X, ⊤)).Opens //
                      Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
                i) :
            (Spec Γ(X, ⊤)).Opens)) :
      Scheme)

Tactic:
rw [Scheme.toSpecΓ_preimage_basicOpen]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsAffine.{u} (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme)

Tactic:
hs₂ _ i.2

Premises used: AlgebraicGeometry.IsAffineOpen, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
affine :
  IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
⊢ IsIso (X :=
    Γ((↑(↑((fun (i : (↑s : Type u)) ↦ ⟨PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)), ⋯⟩) i) :
            (Spec Γ(X, ⊤)).Opens) :
        Scheme),
      ⊤))
    (Scheme.Hom.appTop
      (X.toSpecΓ ∣_
        (↑((fun (i : (↑s : Type u)) ↦
                (Subtype.mk (p := fun (x : (Spec Γ(X, ⊤)).Opens) ↦
                    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x)
                    (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ⋯ :
                  { x : (Spec Γ(X, ⊤)).Opens //
                    Membership.mem (γ := Set (Spec Γ(X, ⊤)).Opens) (Spec Γ(X, ⊤)).affineOpens x }))
              i) :
          (Spec Γ(X, ⊤)).Opens)))

Tactic:
simp only [Opens.map_top, morphismRestrict_app]

Premises used: TopologicalSpace.Opens.map_top, AlgebraicGeometry.morphismRestrict_app
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
IsIso.comp_isIso' ?_ inferInstance

Premises used: Set.Mem, inferInstance, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
affine :
  IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤))
⊢ IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
refine IsIso.comp_isIso' ?_ inferInstance

Premises used: inferInstance, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsIso (X := Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))
    (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))

Tactic:
isIso_ΓSpec_adjunction_unit_app_basicOpen i.1

Premises used: AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
a :
  IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
      (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤)) ↔
    IsIso (X := Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))
      (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))
⊢ IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
    (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤))

Tactic:
convert! isIso_ΓSpec_adjunction_unit_app_basicOpen i.1 using 0

Premises used: AlgebraicGeometry.isIso_ΓSpec_adjunction_unit_app_basicOpen, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ Eq.{u + 1} (α := (Spec Γ(X, ⊤)).Opens) (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤)
    (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this_1 : QuasiSeparatedSpace.{u} ↥X
this : CompactSpace.{u} ↥X
i : (↑s : Type u)
⊢ IsIso (X := Γ((↑(PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Scheme), ⊤))
      (Scheme.Hom.app X.toSpecΓ (Scheme.Opens.ι (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) ''ᵁ ⊤)) ↔
    IsIso (X := Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))
      (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))))

Tactic:
exact congr(IsIso ((ΓSpec.adjunction.unit.app X).app $(by simp)))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
hs₁ :
  Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u)) ''
        s))
    ⊤
hs₃ :
  ∀ (i : (↑Γ((↑U : Scheme), ⊤) : Type u)),
    Membership.mem (γ := Set (↑Γ((↑U : Scheme), ⊤) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) U.topIso.inv) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u)) ''
          s)
        i →
      IsAffineOpen ((↑U : Scheme).basicOpen i)
⊢ IsAffineOpen U

Tactic:
apply isAffine_of_isAffineOpen_basicOpen (U.topIso.inv '' s)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Opens.topIso, Set.image, AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
hs₁ : Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u)) (Ideal.map (CommRingCat.Hom.hom U.topIso.inv) (Ideal.span s)) ⊤
hs₃ :
  Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.map (R := (↑Γ(X, U) : Type u)) (CommRingCat.Hom.hom U.topIso.inv) ⊤) ⊤
hs₄ hs₅ : Eq.{u + 1} (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u)) ⊤ ⊤
⊢ Eq (α := Ideal (↑Γ((↑U : Scheme), ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) U.topIso.inv) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u)) ''
        s))
    ⊤

Tactic:
rw [← Ideal.map_span U.topIso.inv.hom, hs, Ideal.map_top]

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Opens.topIso, Ideal.map_span, Ideal.map_top, CategoryTheory.Iso.inv