awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
simp_rw :
  ∃ (U' : TopologicalSpace.Opens ↥X),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
        {x : TopologicalSpace.Opens ↥X |
          ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)),
            X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
⊢ ∃ (U' : TopologicalSpace.Opens ↥X),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
        {x : TopologicalSpace.Opens ↥X |
          ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
simp_rw [← toSpecΓ_preimage_basicOpen]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
⊢ ∃ (U' : TopologicalSpace.Opens ↥X),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
        {x : TopologicalSpace.Opens ↥X |
          ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)),
            X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
⟨_, ⟨r, ?_, rfl⟩, hxr, (Set.preimage_mono hrU).trans_eq
    (Set.preimage_image_eq _ X.toSpecΓ.isEmbedding.injective)⟩

Premises used: LE.le.trans_eq, AlgebraicGeometry.Scheme.Hom.isEmbedding, Set.preimage_mono, AlgebraicGeometry.Scheme.toSpecΓ, And.intro, Topology.IsEmbedding.injective, Exists.intro, Set.preimage_image_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
refine : IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
⊢ ∃ (U' : TopologicalSpace.Opens ↥X),
    Membership.mem (γ := Set (TopologicalSpace.Opens ↥X))
        {x : TopologicalSpace.Opens ↥X |
          ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)),
            X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U

Tactic:
refine ⟨_, ⟨r, ?_, rfl⟩, hxr, (Set.preimage_mono hrU).trans_eq
    (Set.preimage_image_eq _ X.toSpecΓ.isEmbedding.injective)⟩
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
rw : IsAffineOpen (X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
⊢ IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)

Tactic:
rw [← Hom.isAffineOpen_iff_of_isOpenImmersion X.toSpecΓ]

Premises used: AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
⊢ IsAffineOpen.{u} (X := Spec Γ(X, ⊤)) (PrimeSpectrum.basicOpen r)

Tactic:
IsAffineOpen.Spec_basicOpen r

Premises used: AlgebraicGeometry.IsAffineOpen.Spec_basicOpen
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
h : X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = PrimeSpectrum.basicOpen r
⊢ IsAffineOpen (X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)

Tactic:
convert! IsAffineOpen.Spec_basicOpen r

Premises used: AlgebraicGeometry.IsAffineOpen.Spec_basicOpen
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
⊢ X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = PrimeSpectrum.basicOpen r

Tactic:
SetLike.coe_injective (Set.image_preimage_eq_of_subset
    (hrU.trans (Set.image_subset_range _ _)))

Premises used: HasSubset.Subset.trans, Set.image_subset_range, SetLike.coe_injective, Set.image_preimage_eq_of_subset
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ U
r : (↑Γ(X, ⊤) : Type u)
hxr :
  Membership.mem (α := PrimeSpectrum (↑Γ(X, ⊤) : Type u))
    (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base :
          (a : ↥X) → ↥(Spec Γ(X, ⊤)))
        x :
      ↥(Spec Γ(X, ⊤)))
hrU :
  (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum (↑Γ(X, ⊤) : Type u))) ⊆
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (LocallyRingedSpace.Hom.toShHom (Hom.toLRSHom X.toSpecΓ)).hom.base) :
        (a : ↥X) → ↥(Spec Γ(X, ⊤))) ''
      (↑U : Set ↥X)
⊢ X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = PrimeSpectrum.basicOpen r

Tactic:
exact SetLike.coe_injective (Set.image_preimage_eq_of_subset
    (hrU.trans (Set.image_subset_range _ _)))

Premises used: SetLike.coe_injective
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : IsOpenImmersion X.toSpecΓ
⊢ X.IsQuasiAffine

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
suffices : IsOpenImmersion X.toSpecΓ
⊢ X.IsQuasiAffine

Tactic:
suffices IsOpenImmersion X.toSpecΓ by constructor
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
choose :
  ∀ (r : (x : ↥X) → (↑Γ(X, ⊤) : Type u)) (hr : ∀ (x : ↥X), IsAffineOpen (X.basicOpen (r x)))
    (hxr : ∀ (x : ↥X), x ∈ X.basicOpen (r x)), QuasiSeparatedSpace.{u} ↥X
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
choose r hr hxr using H
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
r : (x : ↥X) → (↑Γ(X, ⊤) : Type u)
hr : ∀ (x : ↥X), IsAffineOpen (X.basicOpen (r x))
hxr : ∀ (x : ↥X), x ∈ X.basicOpen (r x)
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
.of_isOpenCover (U := (X.basicOpen <| r ·))
      (eq_top_iff.mpr fun _ _ ↦ Opens.mem_iSup.mpr ⟨_, hxr _⟩)
      (fun _ ↦ isRetrocompact_basicOpen _) (fun x ↦ (hr _).isQuasiSeparated)

Premises used: Iff.mpr, eq_top_iff, TopologicalSpace.Opens.mem_iSup, AlgebraicGeometry.isRetrocompact_basicOpen, Exists.intro, AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, QuasiSeparatedSpace.of_isOpenCover
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
r : (x : ↥X) → (↑Γ(X, ⊤) : Type u)
hr : ∀ (x : ↥X), IsAffineOpen (X.basicOpen (r x))
hxr : ∀ (x : ↥X), x ∈ X.basicOpen (r x)
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
exact .of_isOpenCover (U := (X.basicOpen <| r ·))
      (eq_top_iff.mpr fun _ _ ↦ Opens.mem_iSup.mpr ⟨_, hxr _⟩)
      (fun _ ↦ isRetrocompact_basicOpen _) (fun x ↦ (hr _).isQuasiSeparated)
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
have : QuasiSeparatedSpace X := by
    choose r hr hxr using H
    exact .of_isOpenCover (U := (X.basicOpen <| r ·))
      (eq_top_iff.mpr fun _ _ ↦ Opens.mem_iSup.mpr ⟨_, hxr _⟩)
      (fun _ ↦ isRetrocompact_basicOpen _) (fun x ↦ (hr _).isQuasiSeparated)
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
⊢ IsOpenImmersion X.toSpecΓ

Tactic:
IsZariskiLocalAtTarget.of_forall_source_exists_preimage _ fun x ↦ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_source_exists_preimage
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
refine :
  ∀ (x : ↥X),
    ∃ (U : (Spec Γ(X, ⊤)).Opens),
      Membership.mem (α := ↥(Spec Γ(X, ⊤))) U (X.toSpecΓ x : ↥(Spec Γ(X, ⊤))) ∧
        IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)
⊢ IsOpenImmersion X.toSpecΓ

Tactic:
refine IsZariskiLocalAtTarget.of_forall_source_exists_preimage _ fun x ↦ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_forall_source_exists_preimage
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
obtain :
  ∀ (r : (↑Γ(X, ⊤) : Type u)) (hr : IsAffineOpen (X.basicOpen r)) (hxr : x ∈ X.basicOpen r),
    ∃ (U : (Spec Γ(X, ⊤)).Opens),
      Membership.mem (α := ↥(Spec Γ(X, ⊤))) U (X.toSpecΓ x : ↥(Spec Γ(X, ⊤))) ∧
        IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)
⊢ ∃ (U : (Spec Γ(X, ⊤)).Opens),
    Membership.mem (α := ↥(Spec Γ(X, ⊤))) U (X.toSpecΓ x : ↥(Spec Γ(X, ⊤))) ∧
      IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)

Tactic:
obtain ⟨r, hr, hxr⟩ := H x
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ ∃ (U : (Spec Γ(X, ⊤)).Opens),
    Membership.mem (α := ↥(Spec Γ(X, ⊤))) U (X.toSpecΓ x : ↥(Spec Γ(X, ⊤))) ∧
      IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)

Tactic:
⟨PrimeSpectrum.basicOpen r, (X.toSpecΓ_preimage_basicOpen r).ge hxr, ?_⟩

Premises used: Eq.ge, PrimeSpectrum.basicOpen, And.intro, Exists.intro, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
refine : IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)
⊢ ∃ (U : (Spec Γ(X, ⊤)).Opens),
    Membership.mem (α := ↥(Spec Γ(X, ⊤))) U (X.toSpecΓ x : ↥(Spec Γ(X, ⊤))) ∧
      IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)

Tactic:
refine ⟨PrimeSpectrum.basicOpen r, (X.toSpecΓ_preimage_basicOpen r).ge hxr, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this_1 : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)

Tactic:
this
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this_1 : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
h : X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
h₁ :
  (↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) : Scheme) = (↑(X.basicOpen r) : Scheme) →
    X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
⊢ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)

Tactic:
convert! this
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this_1 : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
h h₁ : X.basicOpen r = X.basicOpen r
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
rw [toSpecΓ_preimage_basicOpen]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this_1 : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
e_1 : (↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) : Scheme) = (↑(X.basicOpen r) : Scheme)
h h₁ : X.basicOpen r = X.basicOpen r
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r

Tactic:
rw [toSpecΓ_preimage_basicOpen]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
suffices : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
⊢ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)

Tactic:
suffices IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ) by
    convert! this <;> rw [toSpecΓ_preimage_basicOpen]
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
rw :
  IsOpenImmersion (Y := Spec Γ(X, ⊤)) ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
⊢ IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)

Tactic:
rw [← Opens.toSpecΓ_SpecMap_presheaf_map_top]

Premises used: AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)

Tactic:
have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this_1 : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ IsOpenImmersion (Y := Spec Γ(X, ⊤)) ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))

Tactic:
MorphismProperty.comp_mem _ hr.isoSpec.hom _ inferInstance (.of_isLocalization r)

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, Quiver.Hom.unop, inferInstance, CategoryTheory.MorphismProperty.comp_mem, AlgebraicGeometry.IsOpenImmersion.of_isLocalization, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this_1 : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ IsOpenImmersion (Y := Spec Γ(X, ⊤)) ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))

Tactic:
exact MorphismProperty.comp_mem _ hr.isoSpec.hom _ inferInstance (.of_isLocalization r)
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
⊢ CompactSpace.{u} ↥X

Tactic:
have := QuasiCompact.compactSpace_of_compactSpace f
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
⊢ X.IsQuasiAffine

Tactic:
.of_forall_exists_mem_basicOpen _ fun x ↦ ?_

Premises used: AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpen
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
refine : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
⊢ X.IsQuasiAffine

Tactic:
refine .of_forall_exists_mem_basicOpen _ fun x ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
x : ↥X
obtain :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)) (hr : IsAffineOpen (Y.basicOpen r))
    (hxr : Membership.mem (α := ↥Y) (↑(Y.basicOpen r) : Set ↥Y) (f x : ↥Y)),
    ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
⊢ ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r

Tactic:
obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ := (IsQuasiAffine.isBasis_basicOpen
    Y).exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
x : ↥X
r : (↑Γ(Y, ⊤) : Type u)
hr : IsAffineOpen (Y.basicOpen r)
hxr : Membership.mem (α := ↥Y) (↑(Y.basicOpen r) : Set ↥Y) (f x : ↥Y)
⊢ ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r

Tactic:
⟨f.appTop r, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.appTop, Exists.intro, DFunLike.coe