awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
a :
  ⋯.isoSpec.hom ≫
    Spec.map
      (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
a₁ :
  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
a₂ a₃ : CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom
| Spec.map f ∣_ basicOpen r ≫
    ⋯.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)

Tactic:
enter [2, 2, 1]; tactic =>
        change _ = (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op
        ext
        simp only [RingEquiv.toCommRingCatIso_hom,
          AlgEquiv.toRingEquiv_toRingHom, CommRingCat.hom_comp, CommRingCat.hom_ofHom,
          RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes,
          IsAffineOpen.algebraMap_Spec_obj, homOfLE_leOfHom]

Premises used: AlgebraicGeometry.Spec, AlgEquiv.toRingEquiv_toRingHom, Quiver.Hom.op, RingHom.coe_coe, AlgEquiv.commutes, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.Scheme.ΓSpecIso, RingEquiv.toCommRingCatIso_hom, CommRingCat.hom_comp, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CommRingCat.hom_ofHom, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.coe_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Function.comp_apply, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
a :
  ⋯.isoSpec.hom ≫
    Spec.map
      (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
a₁ :
  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)
a₂ a₃ : CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom
| Spec.map f ∣_ basicOpen r ≫
    ⋯.isoSpec.hom ≫
      Spec.map
        (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r)) ≫ e₁.toRingEquiv.toCommRingCatIso.hom)

Tactic:
· enter [2, 2, 1]; tactic =>
        change _ = (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op
        ext
        simp only [RingEquiv.toCommRingCatIso_hom,
          AlgEquiv.toRingEquiv_toRingHom, CommRingCat.hom_comp, CommRingCat.hom_ofHom,
          RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, AlgEquiv.commutes,
          IsAffineOpen.algebraMap_Spec_obj, homOfLE_leOfHom]

Premises used: AlgebraicGeometry.Spec, AlgEquiv.toRingEquiv_toRingHom, Quiver.Hom.op, RingHom.coe_coe, AlgEquiv.commutes, AlgebraicGeometry.IsAffineOpen.algebraMap_Spec_obj, AlgebraicGeometry.Scheme.ΓSpecIso, RingEquiv.toCommRingCatIso_hom, CommRingCat.hom_comp, CategoryTheory.homOfLE_leOfHom, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CommRingCat.hom_ofHom, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, RingHom.coe_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Function.comp_apply, CategoryTheory.Iso.inv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
refine_3 :
  Scheme.Opens.ι (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) ≫
      (Spec S).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso S).inv ≫ Spec.map f =
    (Spec.map f ⁻¹ᵁ basicOpen r).ι ≫ Spec.map f ≫ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv
⊢ Iso.hom (IsAffineOpen.isoSpec ⋯) ≫
      Spec.map (f ≫ (Scheme.ΓSpecIso S).inv ≫ (Spec S).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) =
    Spec.map f ∣_ basicOpen r ≫
      ⋯.isoSpec.hom ≫ Spec.map ((Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
simp only [IsAffineOpen.isoSpec_hom, homOfLE_leOfHom, Spec.map_comp, Category.assoc,
      Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, Scheme.Opens.toSpecΓ_top,
      Scheme.homOfLE_ι_assoc, morphismRestrict_ι_assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.morphismRestrict_ι_assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, AlgebraicGeometry.Scheme.Opens.toSpecΓ_top, CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.Scheme.homOfLE_ι_assoc, AlgebraicGeometry.IsAffineOpen.isoSpec_hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
refine_3 :
  Scheme.Opens.ι (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) ≫ Spec.map f =
    (Spec.map f ⁻¹ᵁ basicOpen r).ι ≫ Spec.map f
⊢ Scheme.Opens.ι (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) ≫
      (Spec S).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso S).inv ≫ Spec.map f =
    (Spec.map f ⁻¹ᵁ basicOpen r).ι ≫ Spec.map f ≫ (Spec R).toSpecΓ ≫ Spec.map (Scheme.ΓSpecIso R).inv

Tactic:
simp only [← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Category.assoc, Iso.inv_hom_id,
      Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, AlgebraicGeometry.SpecMap_ΓSpecIso_hom, CategoryTheory.Category.comp_id, AlgebraicGeometry.Spec.map_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
f : R ⟶ S
r : (↑R : Type u_1)
e₁ : Localization.Away r ≃ₐ[(↑R : Type u_1)] (↑Γ(Spec R, basicOpen r) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(Spec R, basicOpen r) : Type u_1)
e₂ : Localization.Away (M := (↑S : Type u_1))
    ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)) ≃ₐ[(↑S : Type u_1)]
  (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1) :=
  IsLocalization.algEquiv (Submonoid.powers ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r))
    (Localization.Away (M := (↑S : Type u_1))
      ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r : (↑S : Type u_1)))
    (↑Γ(Spec S, basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) : Type u_1)
this :
  IsOpenImmersion.{u_1} (X := Spec (CommRingCat.of (Localization.Away r))) (Y := Spec (CommRingCat.of (↑R : Type u_1)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u_1) (Localization.Away r))))
⊢ Scheme.Opens.ι (basicOpen ((CommRingCat.Hom.hom f : (a : (↑R : Type u_1)) → (↑S : Type u_1)) r)) ≫ Spec.map f =
    (Spec.map f ⁻¹ᵁ basicOpen r).ι ≫ Spec.map f

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine Y
x : ↥X
h :
  ∀ (g : (↑(Y.presheaf.obj (op ⊤)) : Type u_1)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.stalkMap f x) :
              (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                    CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.Γgerm (f x)) :
                  (a : (↑(Y.presheaf.obj (op ⊤)) : Type u_1)) → (↑(Y.presheaf.stalk (f x)) : Type u_1))
                g :
              (↑(Y.presheaf.stalk (f x)) : Type u_1)) :
          (↑(X.presheaf.stalk x) : Type u_1))
        (0 : (↑(X.presheaf.stalk x) : Type u_1)) →
      Eq (α := (↑(Y.presheaf.stalk (f x)) : Type u_1))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.Γgerm (f x)) :
              (a : (↑(Y.presheaf.obj (op ⊤)) : Type u_1)) → (↑(Y.presheaf.stalk (f x)) : Type u_1))
            g :
          (↑(Y.presheaf.stalk (f x)) : Type u_1))
        (0 : (↑(Y.presheaf.stalk (f x)) : Type u_1))
⊢ Function.Injective (α := (↑(Y.presheaf.stalk (f x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap f x)) :
      (a : (↑(Y.presheaf.stalk (f x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
(isAffineOpen_top Y).stalkMap_injective f x trivial h

Premises used: AlgebraicGeometry.isAffineOpen_top, trivial, AlgebraicGeometry.IsAffineOpen.stalkMap_injective
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
a : ⨆ i ∈ s, X.basicOpen i ≤ U
a₁ : U ≤ ⨆ i ∈ s, X.basicOpen i
⊢ ⨆ i ∈ s, X.basicOpen i = U

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
a : ∀ (i : (↑Γ(X, U) : Type u_1)) (j : i ∈ s), X.basicOpen i ≤ U
⊢ ⨆ i ∈ s, X.basicOpen i ≤ U

Tactic:
rw [iSup₂_le_iff]

Premises used: iSup₂_le_iff
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
⊢ ∀ (i : (↑Γ(X, U) : Type u_1)) (j : i ∈ s), X.basicOpen i ≤ U

Tactic:
fun i _ ↦ X.basicOpen_le i

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
⊢ ∀ (i : (↑Γ(X, U) : Type u_1)) (j : i ∈ s), X.basicOpen i ≤ U

Tactic:
exact fun i _ ↦ X.basicOpen_le i

Premises used: AlgebraicGeometry.Scheme.basicOpen_le
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
a :
  ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X)) (hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)),
    Membership.mem (γ := Opens ↥X) (⨆ i ∈ s, X.basicOpen i) x
⊢ Membership.mem (γ := Opens ↥X) (⨆ i ∈ s, X.basicOpen i) x

Tactic:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ := X.isBasis_affineOpens.exists_subset_of_mem_open hx U.2

Premises used: TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ Membership.mem (γ := Opens ↥X) (⨆ i ∈ s, X.basicOpen i) x

Tactic:
SetLike.mem_of_subset ?_ hxV

Premises used: SetLike.mem_of_subset
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
a : (↑V : Set ↥X) ⊆ (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)
⊢ Membership.mem (γ := Opens ↥X) (⨆ i ∈ s, X.basicOpen i) x

Tactic:
refine SetLike.mem_of_subset ?_ hxV

Premises used: SetLike.mem_of_subset
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
rw :
  Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.map
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier)
        (X.presheaf.map
          ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y := (↑U : Set ↥X)))))
      (Ideal.span s))
    ⊤
rw₁ :
  Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.map (R := (↑(X.presheaf.obj (op U)) : Type u_1))
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
        CommRingCat.carrier)
        (X.presheaf.map
          ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y := (↑U : Set ↥X)))))
      ⊤)
    ⊤
rw₂ rw₃ : Eq.{u_1 + 1} (α := Ideal (↑Γ(X, V) : Type u_1)) ⊤ ⊤
⊢ Eq (α := Ideal (↑Γ(X, V) : Type u_1))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier)
              (X.presheaf.map
                ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                  (↑U : Set ↥X))))) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
        s))
    ⊤

Tactic:
rw [← Ideal.map_span, hs, Ideal.map_top]

Premises used: Ideal.map_span, Ideal.map_top
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
a :
  (↑(⨆ (f :
          (↑((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier)
                      (X.presheaf.map
                        ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                          (↑U : Set ↥X))))) :
                  (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
                s) :
            Type u_1)),
          X.basicOpen (↑f : (↑Γ(X, V) : Type u_1))) :
      Set ↥X) ⊆
    (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)
⊢ (↑V : Set ↥X) ⊆ (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)

Tactic:
rw [← (hV.iSup_basicOpen_eq_self_iff (s := X.presheaf.map (homOfLE hVU).op '' s)).mpr
      (by rw [← Ideal.map_span, hs, Ideal.map_top])]

Premises used: Iff.mpr, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
a :
  ∀ (i : (↑(X.presheaf.obj (op U)) : Type u_1)) (i_1 : i ∈ s),
    (↑V : Set ↥X) ∩ (↑(X.basicOpen i) : Set ↥X) ⊆ ⋃ i ∈ s, (↑(X.basicOpen i) : Set ↥X)
⊢ (↑(⨆ (f :
          (↑((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                      CommRingCat.carrier)
                      (X.presheaf.map
                        ((homOfLE (x := (↑V : Set ↥X)) (y := (↑U : Set ↥X)) hVU).op (X := (↑V : Set ↥X)) (Y :=
                          (↑U : Set ↥X))))) :
                  (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op V)) : Type u_1)) ''
                s) :
            Type u_1)),
          X.basicOpen (↑f : (↑Γ(X, V) : Type u_1))) :
      Set ↥X) ⊆
    (↑(⨆ i ∈ s, X.basicOpen i) : Set ↥X)

Tactic:
simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Set.iUnion_coe_set, Set.mem_image,
      Set.iUnion_exists, Set.biUnion_and', Set.iUnion_iUnion_eq_right, Scheme.basicOpen_res,
      Opens.coe_inf, Opens.coe_mk, Set.iUnion_subset_iff]

Premises used: Set.iUnion_iUnion_eq_right, TopologicalSpace.Opens.iSup_mk, Set.iUnion_subset_iff, Set.iUnion_coe_set, Set.mem_image, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe, Set.iUnion_exists, AlgebraicGeometry.Scheme.basicOpen_res, Set.biUnion_and', TopologicalSpace.Opens.coe_inf
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ ∀ (i : (↑(X.presheaf.obj (op U)) : Type u_1)) (i_1 : i ∈ s),
    (↑V : Set ↥X) ∩ (↑(X.basicOpen i) : Set ↥X) ⊆ ⋃ i ∈ s, (↑(X.basicOpen i) : Set ↥X)

Tactic:
fun i hi ↦ (Set.inter_subset_right.trans
      (Set.subset_iUnion₂ (s := fun x _ ↦ (X.basicOpen x : Set X)) i hi))

Premises used: Set.subset_iUnion₂, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u_1)
hs : Eq (α := Ideal (↑Γ(X, U) : Type u_1)) (Ideal.span s) ⊤
x : ↥X
hx : x ∈ U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ (↑U : Set ↥X)
⊢ ∀ (i : (↑(X.presheaf.obj (op U)) : Type u_1)) (i_1 : i ∈ s),
    (↑V : Set ↥X) ∩ (↑(X.basicOpen i) : Set ↥X) ⊆ ⋃ i ∈ s, (↑(X.basicOpen i) : Set ↥X)

Tactic:
exact fun i hi ↦ (Set.inter_subset_right.trans
      (Set.subset_iUnion₂ (s := fun x _ ↦ (X.basicOpen x : Set X)) i hi))

Premises used: Set.subset_iUnion₂, HasSubset.Subset.trans, Set.inter_subset_right
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
obtain :
  ∀ (i : ι) (hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
⊢ ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
obtain ⟨i, hi⟩ := Opens.mem_iSup.mp (iSup_U.ge (Set.mem_univ x))

Premises used: Eq.ge, TopologicalSpace.Opens.mem_iSup, Iff.mp, Set.mem_univ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
P : (↑X.affineOpens : Type u_1) → Prop
ι : Sort u_2
U : ι → (↑X.affineOpens : Type u_1)
iSup_U : Eq.{u_1 + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
V : (↑X.affineOpens : Type u_1)
basicOpen : ∀ (U : (↑X.affineOpens : Type u_1)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : (↑X.affineOpens : Type u_1)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_1)),
    Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_1))) ⊤ →
      (∀ (f : ↥s), P (X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_1)))) → P U
hU : ∀ (i : ι), P (U i)
x : ↥(↑V : X.Opens)
i : ι
hi : (↑x : ↥X) ∈ (↑(U i) : X.Opens)
obtain :
  ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)) (g : (↑Γ(X, (↑(U i) : X.Opens)) : Type u_1))
    (e : X.basicOpen f = X.basicOpen g) (hf : (↑x : ↥X) ∈ X.basicOpen f),
    ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)
⊢ ∃ (f : (↑Γ(X, (↑V : X.Opens)) : Type u_1)), (↑x : ↥X) ∈ X.basicOpen f ∧ P (X.affineBasicOpen f)

Tactic:
obtain ⟨f, g, e, hf⟩ := exists_basicOpen_le_affine_inter V.prop (U i).prop x ⟨x.prop, hi⟩

Premises used: Subtype.prop, And.intro, AlgebraicGeometry.exists_basicOpen_le_affine_inter, Subtype.val