awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Eq (α := Spec (of S) ⟶ pullback.diagonalObj (X := Spec (of S)) (Y := Spec (of R)) (Spec.map (ofHom (algebraMap R S))))
    (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
    (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
have h₀ : Eq (α := Spec (of S) ⟶ Spec (of S))
  (CategoryStruct.comp (Y :=
    pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R S))))
    (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
  (CategoryStruct.comp (Y :=
    pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R S))))
    (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
    (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h₀ :
  Eq (α := Spec (of S) ⟶ Spec (of S))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
⊢ Eq (α := Spec (of S) ⟶ pullback.diagonalObj (X := Spec (of S)) (Y := Spec (of R)) (Spec.map (ofHom (algebraMap R S))))
    (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
    (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
have h₁ : Eq (α := Spec (of S) ⟶ Spec (of S))
  (CategoryStruct.comp (Y :=
    pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R S))))
    (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
    (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
  (CategoryStruct.comp (Y :=
    pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
      (Spec.map (ofHom (algebraMap R S))))
    (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
    (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Eq (α := Spec (of S) ⟶ Spec (of S))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
      (pullback.fst (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
have h₀ : Spec.map (𝟙 (of S)) =
  Spec.map (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))
Tactic: simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Eq (α := Spec (of S) ⟶ Spec (of S))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (pullback.diagonal (Spec.map (ofHom (algebraMap R S))))
      (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
    (CategoryStruct.comp (Y :=
      pullback (X := Spec (of S)) (Y := Spec (of S)) (Z := Spec (of R)) (Spec.map (ofHom (algebraMap R S)))
        (Spec.map (ofHom (algebraMap R S))))
      (Spec.map (ofHom (AlgHom.toRingHom (lmul' R))) ≫ Iso.inv (pullbackSpecIso R S S))
      (pullback.snd (Spec.map (ofHom (algebraMap R S))) (Spec.map (ofHom (algebraMap R S)))))
have h₁ : Spec.map (𝟙 (of S)) =
  Spec.map
    (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
      (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))
Tactic: simp only [pullback.diagonal_fst, pullback.diagonal_snd, ← Spec.map_comp, ← Spec.map_id,
    AlgHom.toRingHom_eq_coe, Category.assoc, pullbackSpecIso_inv_fst, pullbackSpecIso_inv_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Spec.map (𝟙 (of S)) =
    Spec.map (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))
have h₀ : 𝟙 (of S) = CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ 𝟙 (of S) = CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom) (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))
have h₀ : ∀ (x : (↑(of S) : Type u)),
  Eq (α := (↑(of S) : Type u))
    ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom)
              (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
          (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
        x :
      (↑(of S) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : (↑(of S) : Type u)
⊢ Eq (α := (↑(of S) : Type u))
    ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom includeLeftRingHom)
              (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
          (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
        x :
      (↑(of S) : Type u))
have h₀ : x = (lmul' R : (a : S ⊗[R] S) → S) (x ⊗ₜ[R] 1)
Tactic: change x = Algebra.TensorProduct.lmul' R (S := S) (x ⊗ₜ[R] 1)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ Spec.map (𝟙 (of S)) =
    Spec.map
      (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
        (ofHom (↑(lmul' R) : S ⊗[R] S →+* S)))
have h₁ : 𝟙 (of S) =
  CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
    (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ 𝟙 (of S) =
    CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
      (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))
have h₁ : ∀ (x : (↑(of S) : Type u)),
  Eq (α := (↑(of S) : Type u))
    ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
              (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
          (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
        x :
      (↑(of S) : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Pullbacks (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : (↑(of S) : Type u)
⊢ Eq (α := (↑(of S) : Type u))
    ((Hom.hom (𝟙 (of S)) : (a : (↑(of S) : Type u)) → (↑(of S) : Type u)) x : (↑(of S) : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := of (S ⊗[R] S)) (ofHom (↑includeRight : S →+* S ⊗[R] S))
              (ofHom (↑(lmul' R) : S ⊗[R] S →+* S))) :
          (a : (↑(of S) : Type u)) → (↑(of S) : Type u))
        x :
      (↑(of S) : Type u))
have h₁ : x = (lmul' R : (a : S ⊗[R] S) → S) (1 ⊗ₜ[R] x)
Tactic: change x = Algebra.TensorProduct.lmul' R (S := S) (1 ⊗ₜ[R] x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
⊢ IsSeparated (Y := ⊤_ Scheme) (terminal.from X)
have rw : IsSeparated (Y := ⊤_ Scheme) (X.toSpecΓ ≫ terminal.from (Spec Γ(X, ⊤)))
Tactic: rw [← terminal.comp_from X.toSpecΓ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
⊢ IsIso (Hom.ker X.toSpecΓ).subschemeι
have rw : IsIso.{u, u + 1} (X := IdealSheafData.subscheme (X := Spec Γ(X, ⊤)) ⊥) (IdealSheafData.subschemeι ⊥)
Tactic: rw [X.ker_toSpecΓ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
⊢ IsOpenImmersion X.toSpecΓ
have this : IsIso (Hom.imageι X.toSpecΓ)
Tactic: have : IsIso X.toSpecΓ.imageι := by delta Hom.imageι Hom.image; rw [X.ker_toSpecΓ]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : X.IsQuasiAffine
this : IsIso (Hom.imageι X.toSpecΓ)
⊢ IsOpenImmersion X.toSpecΓ
have rw : IsOpenImmersion (Hom.toImage X.toSpecΓ ≫ Hom.imageι X.toSpecΓ)
Tactic: rw [← X.toSpecΓ.toImage_imageι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
⊢ IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))
have rw : IsImmersion (f ≫ Y.toSpecΓ)
Tactic: rw [← toSpecΓ_naturality]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
⊢ X.IsQuasiAffine
have this : IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))
Tactic: have : IsImmersion (X.toSpecΓ ≫ Spec.map f.appTop) := by rw [← toSpecΓ_naturality]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Y.IsQuasiAffine
inst_1 : IsImmersion f
inst_2 : CompactSpace.{u} ↥X
this : IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))
⊢ X.IsQuasiAffine
have this₁ : IsImmersion X.toSpecΓ
Tactic: have : IsImmersion X.toSpecΓ := .of_comp _ (Spec.map f.appTop)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X : Scheme
inst : X.IsQuasiAffine
⊢ Opens.IsBasis.{u} (α := ↥X)
    {x : TopologicalSpace.Opens ↥X | ∃ (r : (↑Γ(X, ⊤) : Type u)) (_ : IsAffineOpen (X.basicOpen r)), X.basicOpen r = x}
have refine : ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X} (hxU : x ∈ 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: refine Opens.isBasis_iff_nbhd.mpr fun {U x} hxU ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X : Scheme
inst : X.IsQuasiAffine
U : TopologicalSpace.Opens ↥X
x : ↥X
hxU : x ∈ 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
have obtain : ∀ (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.basicOpen r)), X.basicOpen r = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
Tactic: obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, hxr, hrU⟩ := (PrimeSpectrum.isBasis_basic_opens
    (R := Γ(X, ⊤))).exists_subset_of_mem_open (Set.mem_image_of_mem _ hxU) (X.toSpecΓ ''ᵁ U).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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.basicOpen r)), X.basicOpen r = x}
        U' ∧
      x ∈ U' ∧ U' ≤ U
have 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
Tactic: simp_rw [← toSpecΓ_preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
have refine : IsAffineOpen (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
Tactic: refine ⟨_, ⟨r, ?_, rfl⟩, hxr, (Set.preimage_mono hrU).trans_eq
    (Set.preimage_image_eq _ X.toSpecΓ.isEmbedding.injective)⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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 (X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
have rw : IsAffineOpen (X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
Tactic: rw [← Hom.isAffineOpen_iff_of_isOpenImmersion X.toSpecΓ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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 (X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r)
have h : X.toSpecΓ ''ᵁ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = PrimeSpectrum.basicOpen r
Tactic: convert! IsAffineOpen.Spec_basicOpen r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
⊢ X.IsQuasiAffine
have suffices : IsOpenImmersion X.toSpecΓ
Tactic: suffices IsOpenImmersion X.toSpecΓ by constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
have 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
Tactic: choose r hr hxr using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
⊢ IsOpenImmersion X.toSpecΓ
have this : 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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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Γ
have refine : ∀ (x : ↥X),
  ∃ (U : (Spec Γ(X, ⊤)).Opens),
    Membership.mem (α := ↥(Spec Γ(X, ⊤))) U (X.toSpecΓ x : ↥(Spec Γ(X, ⊤))) ∧
      IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)
Tactic: refine IsZariskiLocalAtTarget.of_forall_source_exists_preimage _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
⊢ ∃ (U : (Spec Γ(X, ⊤)).Opens),
    Membership.mem (α := ↥(Spec Γ(X, ⊤))) U (X.toSpecΓ x : ↥(Spec Γ(X, ⊤))) ∧
      IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ U).ι ≫ X.toSpecΓ)
have 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Γ)
Tactic: obtain ⟨r, hr, hxr⟩ := H x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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Γ)
have refine : IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)
Tactic: refine ⟨PrimeSpectrum.basicOpen r, (X.toSpecΓ_preimage_basicOpen r).ge hxr, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)
have h : X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
⊢ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)
have h₁ : (↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) : Scheme) = (↑(X.basicOpen r) : Scheme) →
  X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
Tactic: convert! this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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Γ)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
have h : X.basicOpen r = X.basicOpen r
Tactic: rw [toSpecΓ_preimage_basicOpen]