awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier)
            (Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
    ((Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f))

Tactic:
Scheme.basicOpen_res_eq _ _ (eqToHom hU.fromSpec_preimage_self).op

Premises used: Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier)
            (Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
    ((Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f))

Tactic:
exact Scheme.basicOpen_res_eq _ _ (eqToHom hU.fromSpec_preimage_self).op

Premises used: Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_self
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
rw :
  Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f))
    (PrimeSpectrum.basicOpen f)
rw₁ rw₂ :
  Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f))
    ((Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f))
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f

Tactic:
rw [fromSpec_preimage_basicOpen', ← basicOpen_eq_of_affine]

Premises used: AlgebraicGeometry.basicOpen_eq_of_affine, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen'
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
rw : hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f
⊢ hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f

Tactic:
rw [← hU.fromSpec_preimage_basicOpen]

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
h : (↑(hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f) : Set ↥X) = (↑(X.basicOpen f) : Set ↥X)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
h : (↑(X.basicOpen f) : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' (↑(X.basicOpen f) : Set ↥X)) =
    (↑(X.basicOpen f) : Set ↥X)

Tactic:
rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, hU.range_fromSpec]

Premises used: Set.inter_eq_left, Set.image_preimage_eq_inter_range, AlgebraicGeometry.IsAffineOpen.range_fromSpec
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ (↑(X.basicOpen f) : Set ↥X) ⊆ (↑U : Set ↥X)

Tactic:
Scheme.basicOpen_le _ _

Premises used: Set.Mem, AlgebraicGeometry.Scheme.basicOpen_le, Set.Subset
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ (↑(X.basicOpen f) : Set ↥X) ⊆ (↑U : Set ↥X)

Tactic:
exact Scheme.basicOpen_le _ _

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
rw :
  (Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f) =
    hU.fromSpec ⁻¹ᵁ X.basicOpen f
rw₁ rw₂ :
  Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
⊢ Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
    (PrimeSpectrum.basicOpen f)

Tactic:
rw [← hU.fromSpec_preimage_basicOpen, Scheme.preimage_basicOpen]

Premises used: AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
rw : IsAffineOpen.{u} (X := Spec Γ(X, U)) (PrimeSpectrum.basicOpen f)
⊢ IsAffineOpen (X.basicOpen f)

Tactic:
rw [← hU.fromSpec_image_basicOpen, Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion]

Premises used: AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsAffineOpen.{u} (X := Spec (CommRingCat.of (↑Γ(X, U) : Type u)))
    (Scheme.Hom.opensRange (X := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U) : Type u) (Localization.Away f)))))

Tactic:
isAffineOpen_opensRange
      (Spec.map (CommRingCat.ofHom <| algebraMap Γ(X, U) (Localization.Away f)))

Premises used: CommRingCat.carrier, Algebra.algebraMap, AlgebraicGeometry.isAffineOpen_opensRange, Localization.Away, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
h :
  Spec Γ(X, U) = Spec (CommRingCat.of (↑Γ(X, U) : Type u)) →
    PrimeSpectrum.basicOpen f =
      Scheme.Hom.opensRange (X := Spec (CommRingCat.of (Localization.Away f)))
        (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U) : Type u) (Localization.Away f))))
⊢ IsAffineOpen.{u} (X := Spec Γ(X, U)) (PrimeSpectrum.basicOpen f)

Tactic:
convert!
    isAffineOpen_opensRange
      (Spec.map (CommRingCat.ofHom <| algebraMap Γ(X, U) (Localization.Away f)))

Premises used: CommRingCat.carrier, Algebra.algebraMap, AlgebraicGeometry.isAffineOpen_opensRange, Localization.Away, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 : Spec Γ(X, U) = Spec (CommRingCat.of (↑Γ(X, U) : Type u))
⊢ PrimeSpectrum.basicOpen f =
    Scheme.Hom.opensRange (X := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U) : Type u) (Localization.Away f))))

Tactic:
Opens.ext (PrimeSpectrum.localization_away_comap_range (Localization.Away f) f).symm

Premises used: Localization.Away, TopologicalSpace.Opens.ext, Eq.symm, PrimeSpectrum.localization_away_comap_range
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 : Spec Γ(X, U) = Spec (CommRingCat.of (↑Γ(X, U) : Type u))
⊢ PrimeSpectrum.basicOpen f =
    Scheme.Hom.opensRange (X := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U) : Type u) (Localization.Away f))))

Tactic:
exact Opens.ext (PrimeSpectrum.localization_away_comap_range (Localization.Away f) f).symm

Premises used: TopologicalSpace.Opens.ext
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
⊢ IsAffineOpen.{u_1} (X := Spec R) (PrimeSpectrum.basicOpen f)

Tactic:
basicOpen_eq_of_affine f ▸ (isAffineOpen_top (Spec <| .of R)).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Spec, CommRingCat.carrier, AlgebraicGeometry.IsAffineOpen.basicOpen, Eq.rec, CommRingCat.of, AlgebraicGeometry.basicOpen_eq_of_affine
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
inst : IsAffine X
r : (↑Γ(X, ⊤) : Type u)
⊢ IsAffine.{u} (↑(X.basicOpen r) : Scheme)

Tactic:
(isAffineOpen_top X).basicOpen _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.IsAffineOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : (↑Γ(X, ⊤) : Type u)
apply : IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
apply (X.basicOpen r).ι.isAffineOpen_iff_of_isOpenImmersion.mp

Premises used: AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.basicOpen, Iff.mp, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : (↑Γ(X, ⊤) : Type u)
rw :
  IsAffineOpen
    (X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, U)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r))
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
rw [Scheme.Hom.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι, inf_comm,
    ← Scheme.basicOpen_res _ _ (homOfLE le_top).op]

Premises used: Quiver.Hom.op, AlgebraicGeometry.Scheme.Hom.image_preimage_eq_opensRange_inf, AlgebraicGeometry.Scheme.Opens.opensRange_ι, inf_comm, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.basicOpen_res
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : (↑Γ(X, ⊤) : Type u)
⊢ IsAffineOpen
    (X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, U)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r))

Tactic:
hU.basicOpen _

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : (↑Γ(X, ⊤) : Type u)
⊢ IsAffineOpen
    (X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, U)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, U) : Type u))
        r))

Tactic:
exact hU.basicOpen _

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
⊢ IsAffine.{u} (↑U : Scheme)

Tactic:
have : IsAffine _ := hU
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
obtain :
  ∀ (r : (↑Γ((↑U : Scheme), ⊤) : Type u))
    (h₁ : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (↑x : ↥X) h ∈ (↑((↑U : Scheme).basicOpen r) : Set ↥(↑U : Scheme)))
    (h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V),
    ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f
⊢ ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f

Tactic:
obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, h₁, h₂ : _ ≤ U.ι ⁻¹ᵁ V⟩ :=
    (isBasis_basicOpen U).exists_subset_of_mem_open (x.2 : (⟨x, h⟩ : U) ∈ _) (U.ι ⁻¹ᵁ V).isOpen

Premises used: AlgebraicGeometry.isBasis_basicOpen, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopologicalSpace.Opens.isOpen, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.Opens.toScheme, CategoryTheory.Functor.obj, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₁ : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (↑x : ↥X) h ∈ (↑((↑U : Scheme).basicOpen r) : Set ↥(↑U : Scheme))
h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V
⊢ (↑x : ↥X) ∈ X.basicOpen r

Tactic:
simpa [U.mem_basicOpen_toScheme] using h₁

Premises used: AlgebraicGeometry.Scheme.Opens.mem_basicOpen_toScheme
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₁ : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (↑x : ↥X) h ∈ (↑((↑U : Scheme).basicOpen r) : Set ↥(↑U : Scheme))
h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V
⊢ (↑x : ↥X) ∈ X.basicOpen r

Tactic:
replace h₁ : x.1 ∈ X.basicOpen r := by simpa [U.mem_basicOpen_toScheme] using h₁
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V
h₁ : (↑x : ↥X) ∈ X.basicOpen r
⊢ X.basicOpen r ≤ V

Tactic:
simpa [Scheme.image_basicOpen] using (U.ι.image_mono h₂).trans (U.ι.image_preimage_le _)

Premises used: AlgebraicGeometry.Scheme.Hom.image_preimage_le, AlgebraicGeometry.Scheme.Hom.image_mono, AlgebraicGeometry.Scheme.image_basicOpen, AlgebraicGeometry.Scheme.Opens.ι, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V
h₁ : (↑x : ↥X) ∈ X.basicOpen r
⊢ X.basicOpen r ≤ V

Tactic:
replace h₂ : X.basicOpen r ≤ V := by
    simpa [Scheme.image_basicOpen] using (U.ι.image_mono h₂).trans (U.ι.image_preimage_le _)
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₁ : (↑x : ↥X) ∈ X.basicOpen r
h₂ : X.basicOpen r ≤ V
⊢ X.basicOpen (U := U)
        ((CommRingCat.Hom.hom U.topIso.hom : (a : (↑Γ((↑U : Scheme), ⊤) : Type u)) → (↑Γ(X, U) : Type u)) r) ≤
      V ∧
    (↑x : ↥X) ∈
      X.basicOpen (U := U)
        ((CommRingCat.Hom.hom U.topIso.hom : (a : (↑Γ((↑U : Scheme), ⊤) : Type u)) → (↑Γ(X, U) : Type u)) r)

Tactic:
simp [Scheme.Opens.toScheme_presheaf_obj, h₁, h₂]

Premises used: AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₁ : (↑x : ↥X) ∈ X.basicOpen r
h₂ : X.basicOpen r ≤ V
⊢ ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f

Tactic:
exact ⟨U.topIso.hom.hom r, by simp [Scheme.Opens.toScheme_presheaf_obj, h₁, h₂]⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R : CommRingCat
U : (Spec R).Opens
⊢ Eq (α := (↑R : Type u_1) →+* (↑Γ(Spec R, U) : Type u_1)) (algebraMap (↑R : Type u_1) (↑Γ(Spec R, U) : Type u_1))
    (CommRingCat.Hom.hom ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯))))

Tactic:
rfl

Premises used: Set.Mem, setOf, AlgebraicGeometry.StructureSheaf.sectionsSubalgebra, RingHom.codRestrict, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f_1 : (↑Γ(X, U) : Type u)
R : CommRingCat
f : (↑R : Type u_1)
⊢ IsLocalization.Away f (↑Γ(Spec R, PrimeSpectrum.basicOpen f) : Type u_1)

Tactic:
inferInstanceAs (IsLocalization.Away f
    ((Spec.structureSheaf R).obj.obj (op <| PrimeSpectrum.basicOpen f)))

Premises used: _private.0.AlgebraicGeometry.IsAffineOpen.instAwayCarrierObjOppositeOpensCarrierCarrierCommRingCatSpecPresheafOpOpensBasicOpen._proof_1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsIso (hU.basicOpenSectionsToAffine f)

Tactic:
(hU.fromSpec.isIso_app _ (hU.opensRange_fromSpec.symm ▸ X.basicOpen_le f)).comp_isIso'
    inferInstance

Premises used: inferInstance, AlgebraicGeometry.IsAffineOpen.fromSpec, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine, AlgebraicGeometry.Scheme.Hom.isIso_app, CategoryTheory.IsIso.comp_isIso'
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
basicOpenSectionsToAffine : IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
apply
    (IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers f)
      (asIso <| basicOpenSectionsToAffine hU f).commRingCatIsoToRingEquiv).mpr

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, Iff.mpr, IsLocalization.isLocalization_iff_of_ringEquiv, AlgebraicGeometry.IsAffineOpen.basicOpenSectionsToAffine, Submonoid.powers, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsLocalization.Away f
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u)

Tactic:
StructureSheaf.IsLocalization.to_basicOpen _ f

Premises used: AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
h :
  (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
              (structureSheaf (↑Γ(X, U) : Type u)))
            (op (PrimeSpectrum.basicOpen f))) :
        Type u) →
    HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
        CommSemiring
          (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
                (ObjectProperty.FullSubcategory.obj (P :=
                  Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
                  (structureSheaf (↑Γ(X, U) : Type u)))
                (op (PrimeSpectrum.basicOpen f))) :
            Type u))
        CommRing.toCommSemiring →
      RingHom.toAlgebra
          ((asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
            (algebraMap (↑Γ(X, U) : Type u) (↑Γ(X, X.basicOpen f) : Type u))) =
        StructureSheaf.openAlgebra (↑Γ(X, U) : Type u) (op (PrimeSpectrum.basicOpen f))
⊢ IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)

Tactic:
convert! StructureSheaf.IsLocalization.to_basicOpen _ f using 1

Premises used: AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen