awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
z : ↥(pullback f q)
hz : z ∈ Z
hzt : fT z = t
⊢ Membership.mem (α := ↥X) (U (Scheme.Cover.idx 𝒰 (p z))) (p z : ↥X)

Tactic:
simpa [U] using 𝒰.covers (p z)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Cover.covers, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
z : ↥(pullback f q)
hz : z ∈ Z
hzt : fT z = t
⊢ ∃ (i : 𝒰.I₀), Membership.mem (α := ↥T) (Ti i) (fT z : ↥T) ∧ Membership.mem (α := ↥X) (U i) (p z : ↥X)

Tactic:
exact ⟨𝒰.idx (p z), hzt ▸ ht _, by simpa [U] using 𝒰.covers (p z)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
⊢ t ∈ Zc

Tactic:
have htZc : t ∈ Zc := by
    intro ⟨z, hz, hzt⟩
    suffices ∃ i, fT z ∈ Ti i ∧ p z ∈ U i from hz (by simpa)
    exact ⟨𝒰.idx (p z), hzt ▸ ht _, by simpa [U] using 𝒰.covers (p z)⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
obtain :
  ∀ (g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))
    (htU' :
      Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t)
    (hU'le : basicOpen g ≤ Zc), CompactSpace.{u} ↥X
⊢ CompactSpace.{u} ↥X

Tactic:
obtain ⟨U', ⟨g, rfl⟩, htU', hU'le⟩ := Opens.isBasis_iff_nbhd.mp isBasis_basic_opens htZc

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd, Iff.mp, PrimeSpectrum.isBasis_basic_opens, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
⊢ Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'

Tactic:
have ht'g : t' ∈ PrimeSpectrum.basicOpen g :=
    show φ g ∉ t.asIdeal from (show φ g = g from aeval_ite_mem_eq_self g subset_rfl).symm ▸ htU'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
⊢ t' ∉ ⇑fT '' Z

Tactic:
have h : t' ∉ fT '' Z := hU'le ht'g
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
h : t' ∉ ⇑fT '' Z
suffices : Eq.{u + 1} (α := Set ↥X) (⋃ i ∈ σ, (U i).carrier) Set.univ
⊢ CompactSpace.{u} ↥X

Tactic:
suffices ⋃ i ∈ σ, (U i).1 = Set.univ from
    ⟨this ▸ Finset.isCompact_biUnion _ fun i _ ↦ isCompact_range (𝒰.f i).continuous⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
h : t' ∉ ⇑fT '' Z
rw : ∀ (a : ↥X), ∃ (i : 𝒰.I₀) (_ : i ∈ σ), a ∈ (U i).carrier
⊢ Eq.{u + 1} (α := Set ↥X) (⋃ i ∈ σ, (U i).carrier) Set.univ

Tactic:
rw [Set.iUnion₂_eq_univ_iff]

Premises used: Set.iUnion₂_eq_univ_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
h : t' ∉ ⇑fT '' Z
contrapose! :
  ∀ (h : ∃ (a : ↥X), ∀ (i : 𝒰.I₀) (j : i ∈ σ), a ∉ (U i).carrier), Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
⊢ ∀ (a : ↥X), ∃ (i : 𝒰.I₀) (_ : i ∈ σ), a ∈ (U i).carrier

Tactic:
contrapose! h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
h : ∃ (a : ↥X), ∀ (i : 𝒰.I₀) (j : i ∈ σ), a ∉ (U i).carrier
obtain : ∀ (x : ↥X) (hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), x ∉ (U i).carrier), Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
⊢ Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'

Tactic:
obtain ⟨x, hx⟩ := h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
x : ↥X
hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), x ∉ (U i).carrier
obtain :
  ∀ (z : ↥(pullback f q)) (hzr : (pullback.snd f q) z = t')
    (hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), ((pullback.fst f q) z : ↥X) ∉ (U i).carrier),
    Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'
⊢ Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'

Tactic:
obtain ⟨z, rfl, hzr⟩ := exists_preimage_pullback x t' (Subsingleton.elim (f x) (q t'))

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Subsingleton.elim, DFunLike.coe, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), ((pullback.fst f q) z : ↥X) ∉ (U i).carrier
this :
  ∀ (i : 𝒰.I₀),
    Membership.mem (γ := Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
        ((Opens.comap
                { toFun := comap φ, continuous_toFun := ⋯ :
                  C(PrimeSpectrum (MvPolynomial 𝒰.I₀ K), PrimeSpectrum (MvPolynomial 𝒰.I₀ K)) } :
              (a : Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K))) → Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
            (Ti i) :
          Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
        t →
      (p z : ↥X) ∉ U i
⊢ z ∈ Z

Tactic:
simpa [Z, p, fT, hzr]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), ((pullback.fst f q) z : ↥X) ∉ (U i).carrier
suffices :
  ∀ (i : 𝒰.I₀),
    Membership.mem (γ := Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
        ((Opens.comap
                { toFun := comap φ, continuous_toFun := ⋯ :
                  C(PrimeSpectrum (MvPolynomial 𝒰.I₀ K), PrimeSpectrum (MvPolynomial 𝒰.I₀ K)) } :
              (a : Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K))) → Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
            (Ti i) :
          Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
        t →
      (p z : ↥X) ∉ U i
⊢ Membership.mem (γ := Set ↥T) (⇑fT '' Z) t'

Tactic:
suffices ∀ i, t ∈ (Ti i).comap ⟨_, continuous_comap φ⟩ → p z ∉ U i from
    ⟨z, by simpa [Z, p, fT, hzr], hzr⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X : Scheme
K : Type u
inst : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst_1 : UniversallyClosed f
𝒰 : X.OpenCover := X.affineCover
U : (i : 𝒰.I₀) → X.Opens := fun (i : 𝒰.I₀) ↦ Scheme.Hom.opensRange (𝒰.f i)
T : Scheme := Spec (CommRingCat.of (MvPolynomial 𝒰.I₀ K))
q : T ⟶ Spec (CommRingCat.of K) := Spec.map (CommRingCat.ofHom C)
Ti : (i : 𝒰.I₀) → T.Opens := fun (i : 𝒰.I₀) ↦ basicOpen (MvPolynomial.X i)
fT : pullback f q ⟶ T := pullback.snd f q
p : pullback f q ⟶ X := pullback.fst f q
Z : Set ↥(pullback f q) := (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))ᶜ
hZ : IsClosed Z
Zc : T.Opens := { carrier := (⇑fT '' Z)ᶜ, is_open' := ⋯ }
ψ : MvPolynomial 𝒰.I₀ K →ₐ[K] K := aeval fun (x : 𝒰.I₀) ↦ 1
t : ↥T := (Spec.map (CommRingCat.ofHom ψ.toRingHom)) default
ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
htZc : t ∈ Zc
g : (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u)
htU' : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t
hU'le : basicOpen g ≤ Zc
σ : Finset 𝒰.I₀ := vars g
φ : MvPolynomial 𝒰.I₀ K →+* MvPolynomial 𝒰.I₀ K :=
  AlgHom.toRingHom (aeval fun (i : 𝒰.I₀) ↦ if i ∈ σ then MvPolynomial.X i else 0)
t' : ↥T := (Spec.map (CommRingCat.ofHom φ)) t
ht'g : Membership.mem (γ := Opens (PrimeSpectrum (↑(CommRingCat.of (MvPolynomial 𝒰.I₀ K)) : Type u))) (basicOpen g) t'
z : ↥(pullback f q)
hzr : (pullback.snd f q) z = t'
hx : ∀ (i : 𝒰.I₀) (j : i ∈ σ), ((pullback.fst f q) z : ↥X) ∉ (U i).carrier
i : 𝒰.I₀
hi₁ :
  Membership.mem (γ := Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
    (basicOpen ((φ : (a : MvPolynomial 𝒰.I₀ K) → MvPolynomial 𝒰.I₀ K) (MvPolynomial.X i)) :
      Opens (PrimeSpectrum (MvPolynomial 𝒰.I₀ K)))
    t
hi₂ : Membership.mem (α := ↥X) (U i) (p z : ↥X)
⊢ Eq (α := MvPolynomial 𝒰.I₀ K)
    ((φ : (a : MvPolynomial 𝒰.I₀ K) → MvPolynomial 𝒰.I₀ K) (MvPolynomial.X i) : MvPolynomial 𝒰.I₀ K)
    (0 : MvPolynomial 𝒰.I₀ K)

Tactic:
simpa [φ] using (hx i · hi₂)