awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
rw :
  (∀ (x : ↥(Spec R)),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
        Membership.mem (γ := Set ↥(Spec R))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          i)
⊢ Membership.mem (γ := Set (Presieve (Spec R))) ((precoverage IsOpenImmersion).coverings (Spec R))
    (PreZeroHypercover.presieve₀
      { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
        f := fun (r : (↑R : Type u)) ↦ Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) })

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
⊢ (∀ (x : ↥(Spec R)),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
        Membership.mem (γ := Set ↥(Spec R))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          i)

Tactic:
⟨fun x ↦ ⟨1, ?_⟩, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway⟩

Premises used: AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
refine :
  ∀ (x : ↥(Spec R)),
    Membership.mem (γ := Set ↥(Spec R))
      (Set.range (ι :=
        ↥(PreZeroHypercover.X (S := Spec R)
            { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun (r : (↑R : Type u)) ↦
                Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
              PreZeroHypercover (Spec R) }
            1))
        ⇑(PreZeroHypercover.f
            { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun (r : (↑R : Type u)) ↦
                Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
            1))
      x
⊢ (∀ (x : ↥(Spec R)),
      ∃ (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
        Membership.mem (γ := Set ↥(Spec R))
          (Set.range (ι :=
            ↥(PreZeroHypercover.X
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
            ⇑(PreZeroHypercover.f
                { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                  f := fun (r : (↑R : Type u)) ↦
                    Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                  PreZeroHypercover (Spec R) }
                i))
          x) ∧
    ∀
      (i :
        PreZeroHypercover.I₀ (C := Scheme) (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }),
      IsOpenImmersion
        (PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          i)

Tactic:
refine ⟨fun x ↦ ⟨1, ?_⟩, AlgebraicGeometry.Scheme.isOpenImmersion_SpecMap_localizationAway⟩
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
rw : Membership.mem (γ := Set ↥(Spec R)) Set.univ x
rw₁ :
  Epi.{u, u + 1} (X :=
    (↑(toLocallyRingedSpace
            (PreZeroHypercover.X (S := Spec R)
              { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                f := fun (r : (↑R : Type u)) ↦
                  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                PreZeroHypercover (Spec R) }
              1)).toPresheafedSpace :
      TopCat))
    (Y := (↑(Spec R).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base
      (LocallyRingedSpace.Hom.toHom
        (Hom.toLRSHom'
          (PreZeroHypercover.f
            { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun (r : (↑R : Type u)) ↦
                Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
            1))))
⊢ Membership.mem (γ := Set ↥(Spec R))
    (Set.range (ι :=
      ↥(PreZeroHypercover.X (S := Spec R)
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
            PreZeroHypercover (Spec R) }
          1))
      ⇑(PreZeroHypercover.f
          { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
            f := fun (r : (↑R : Type u)) ↦
              Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
          1))
    x

Tactic:
rw [Set.range_eq_univ.mpr ((TopCat.epi_iff_surjective _).mp _)]

Premises used: Iff.mpr, Set.range_eq_univ, Iff.mp, TopCat.epi_iff_surjective
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ Membership.mem (γ := Set ↥(Spec R)) Set.univ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ Membership.mem (γ := Set ↥(Spec R)) Set.univ x

Tactic:
exact trivial

Premises used: trivial
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
x : ↥(Spec R)
⊢ Epi.{u, u + 1} (X :=
    (↑(toLocallyRingedSpace
            (PreZeroHypercover.X (S := Spec R)
              { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
                f := fun (r : (↑R : Type u)) ↦
                  Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) :
                PreZeroHypercover (Spec R) }
              1)).toPresheafedSpace :
      TopCat))
    (Y := (↑(Spec R).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base
      (LocallyRingedSpace.Hom.toHom
        (Hom.toLRSHom'
          (PreZeroHypercover.f
            { I₀ := (↑R : Type u), X := fun (r : (↑R : Type u)) ↦ Spec (CommRingCat.of (Localization.Away r)),
              f := fun (r : (↑R : Type u)) ↦
                Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (Localization.Away r))) }
            1))))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
i : X.affineBasisCover.I₀
⊢ X.affineBasisCover.X i = Spec (X.affineBasisCoverRing i)

Tactic:
rfl

Premises used: AlgebraicGeometry.Spec, Set.Mem, AlgebraicGeometry.Scheme.affineBasisCoverRing, rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
h_open :
  ∀ (u : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        u →
      IsOpen u
h_nhds :
  ∀ (a : ↥X) (u : Set ↥X),
    a ∈ u →
      IsOpen u →
        ∃ (v : Set ↥X),
          Membership.mem (γ := Set (Set ↥X))
              {x : Set ↥X |
                ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
              v ∧
            a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u} (α := ↥X)
    {x : Set ↥X |
      ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}

Tactic:
apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : X.affineBasisCover.I₀
⊢ IsOpen (X := ↥X) (Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a))

Tactic:
IsOpenImmersion.isOpen_range (X.affineBasisCover.f a)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.affineBasisCover, AlgebraicGeometry.IsOpenImmersion.isOpen_range, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : X.affineBasisCover.I₀
⊢ IsOpen (X := ↥X) (Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a))

Tactic:
exact IsOpenImmersion.isOpen_range (X.affineBasisCover.f a)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.affineBasisCover, AlgebraicGeometry.IsOpenImmersion.isOpen_range, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
h_nhds :
  ∀ (x : ↥(X.affineCover.X (Cover.idx X.affineCover a))) (e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a),
    ∃ (v : Set ↥X),
      Membership.mem (γ := Set (Set ↥X))
          {x : Set ↥X |
            ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
          v ∧
        a ∈ v ∧ v ⊆ U
⊢ ∃ (v : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        v ∧
      a ∈ v ∧ v ⊆ U

Tactic:
rcases X.affineCover.covers a with ⟨x, e⟩

Premises used: AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
rw :
  ∀ (haU : Membership.mem (α := ↥X) U ((X.affineCover.f (Cover.idx X.affineCover a)) x : ↥X))
    (e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a),
    let U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U;
    x ∈ U'
⊢ x ∈ U'

Tactic:
rw [← e] at haU
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
haU : Membership.mem (α := ↥X) U ((X.affineCover.f (Cover.idx X.affineCover a)) x : ↥X)
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'

Tactic:
haU

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
haU : Membership.mem (α := ↥X) U ((X.affineCover.f (Cover.idx X.affineCover a)) x : ↥X)
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'

Tactic:
exact haU
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'

Tactic:
have hxU' : x ∈ U' := by rw [← e] at haU; exact haU
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s :
  (↑((fun (x : (↑X.toTopCat : Type u)) ↦
          Classical.choose (p := fun (R : CommRingCat.{u}) ↦
            Nonempty.{u + 1}
              (X.restrict (U :=
                  Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                            Classical.choose (p := fun (U : OpenNhds x) ↦
                              ∃ (R : CommRingCat.{u}),
                                Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)
                          x) :
                      TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                  (f :=
                  (Opens.inclusion'
                      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                ∃ (R : CommRingCat.{u}),
                                  Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯)
                            x) :
                        TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                    Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                      X.toTopCat))
                  ⋯ ≅
                Spec.toLocallyRingedSpace.obj (op R)))
            ⋯)
        (Cover.idx X.affineCover a)) :
    Type u)
hxV :
  x ∈
    (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u)))
hVU :
  (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
    U'
⊢ ∃ (v : Set ↥X),
    Membership.mem (γ := Set (Set ↥X))
        {x : Set ↥X |
          ∃ (a : X.affineBasisCover.I₀), x = Set.range (ι := ↥(X.affineBasisCover.X a)) ⇑(X.affineBasisCover.f a)}
        v ∧
      a ∈ v ∧ v ⊆ U

Tactic:
⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩

Premises used: And.intro, Exists.intro, Sigma.mk, rfl
-- Module: Mathlib.AlgebraicGeometry.Cover.Open
Goal:
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s :
  (↑((fun (x : (↑X.toTopCat : Type u)) ↦
          Classical.choose (p := fun (R : CommRingCat.{u}) ↦
            Nonempty.{u + 1}
              (X.restrict (U :=
                  Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                    (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                            Classical.choose (p := fun (U : OpenNhds x) ↦
                              ∃ (R : CommRingCat.{u}),
                                Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                              ⋯)
                          x) :
                      TopologicalSpace.Opens (↑X.toTopCat : Type u)))
                  (f :=
                  (Opens.inclusion'
                      (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                              Classical.choose (p := fun (U : OpenNhds x) ↦
                                ∃ (R : CommRingCat.{u}),
                                  Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                ⋯)
                            x) :
                        TopologicalSpace.Opens (↑X.toTopCat : Type u)) :
                    Functor.obj (C := TopologicalSpace.Opens (↑X.toTopCat : Type u)) (Opens.toTopCat X.toTopCat)
                        (↑((fun (x : (↑X.toTopCat : Type u)) ↦
                                Classical.choose (p := fun (U : OpenNhds x) ↦
                                  ∃ (R : CommRingCat.{u}),
                                    Nonempty.{u + 1} (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)))
                                  ⋯)
                              x) :
                          TopologicalSpace.Opens (↑X.toTopCat : Type u)) ⟶
                      X.toTopCat))
                  ⋯ ≅
                Spec.toLocallyRingedSpace.obj (op R)))
            ⋯)
        (Cover.idx X.affineCover a)) :
    Type u)
hxV :
  x ∈
    (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u)))
hVU :
  (↑(PrimeSpectrum.basicOpen s) :
      Set
        (PrimeSpectrum
          (↑((fun (x : (↑X.toTopCat : Type u)) ↦ Classical.choose ⋯) (Cover.idx X.affineCover a)) : Type u))) ⊆
    U'
⊢ Membership.mem (γ := Set ↥X)
    (Set.image (α := ↥(X.affineCover.X (Cover.idx X.affineCover a))) (⇑(X.affineCover.f (Cover.idx X.affineCover a)))
      (Opens.carrier (PrimeSpectrum.basicOpen s)))
    a

Tactic:
⟨x, hxV, e⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image