awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : f x ⤳ y
i : ι
hi : y ∈ U i
⊢ y ∈ f '' closure[inst] {x}
have hfx : f x ∈ U i
Tactic: have hfx : f x ∈ U i := (U i).2.stableUnderGeneralization hy hi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
⊢ Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
have simp : Membership.mem (γ := Set β) (closure[inst_1] {f x}) y
Tactic: simp only [closure_subtype, Set.image_singleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
⊢ y ∈ f '' closure[inst] {x}
have hy₁ : Membership.mem (γ := Set ↥(U i))
  (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
  (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
Tactic: have hy : (⟨y, hi⟩ : U i) ∈ closure {⟨f x, hfx⟩} := by
      simp only [closure_subtype, Set.image_singleton]
      rwa [← specializes_iff_mem_closure]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (goal)
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy_1 : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy :
  Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
⊢ y ∈ f '' closure[inst] {x}
have hP₃ : ∀ (a : (↑(f ⁻¹' (U i).carrier) : Type u_1))
  (ha :
    Membership.mem (γ := Set (↑(f ⁻¹' (U i).carrier) : Type u_1))
      (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hfx}) a)
  (hay : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi), y ∈ f '' closure[inst] {x}
Tactic: obtain ⟨a, ha, hay⟩ := hsp i ⟨x, hfx⟩ hy
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy_1 : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy :
  Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
a : (↑(f ⁻¹' (U i).carrier) : Type u_1)
ha :
  Membership.mem (γ := Set (↑(f ⁻¹' (U i).carrier) : Type u_1))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hfx}) a
hay : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi
⊢ y ∈ f '' closure[inst] {x}
have ha₁ : Membership.mem (γ := Set α)
  (closure[inst]
    (Set.image (α := { a : α // a ∈ f ⁻¹' (U i).carrier }) (Subtype.val (p := fun (a : α) ↦ a ∈ f ⁻¹' (U i).carrier))
      {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hfx}))
  (↑a : α)
Tactic: rw [closure_subtype] at ha
Cleared hypotheses: ha, hay
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy_1 : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy :
  Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
a : (↑(f ⁻¹' (U i).carrier) : Type u_1)
ha :
  Membership.mem (γ := Set α)
    (closure[inst]
      (Set.image (α := { a : α // a ∈ f ⁻¹' (U i).carrier }) (Subtype.val (p := fun (a : α) ↦ a ∈ f ⁻¹' (U i).carrier))
        {Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' (U i).carrier) x hfx}))
    (↑a : α)
hay : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi
⊢ y ∈ f '' closure[inst] {x}
have ha₁ : Membership.mem (γ := Set α) (closure[inst] {x}) (↑a : α)
Tactic: simp only [Opens.carrier_eq_coe, Set.image_singleton] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap (hypothesis)
Goal:
α β : Type u_1
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
ι : Type u_1
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst, inst_1] f
hsp :
  ∀ (i : ι) (x : (↑(f ⁻¹' (U i).carrier) : Type u_1)),
    closure[instTopologicalSpaceSubtype] {(U i).carrier.restrictPreimage f x} ⊆
      (U i).carrier.restrictPreimage f '' closure[instTopologicalSpaceSubtype] {x}
x : α
y : β
hy_1 : f x ⤳ y
i : ι
hi : y ∈ U i
hfx : f x ∈ U i
hy :
  Membership.mem (γ := Set ↥(U i))
    (closure[instTopologicalSpaceSubtype] {Subtype.mk (p := fun (x : β) ↦ x ∈ U i) (f x) hfx})
    (Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi)
a : (↑(f ⁻¹' (U i).carrier) : Type u_1)
hay : (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi
ha : Membership.mem (γ := Set α) (closure[inst] {x}) (↑a : α)
⊢ y ∈ f '' closure[inst] {x}
have hay₁ : (↑((U i).carrier.restrictPreimage f a) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi) : β)
Tactic: apply_fun Subtype.val at hay
Cleared hypotheses: hay
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
⊢ @UniversallyClosed = (topologically @IsClosedMap).universally
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y), UniversallyClosed f ↔ (topologically @IsClosedMap).universally f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ UniversallyClosed f ↔ (topologically @IsClosedMap).universally f
have h : (topologically @IsClosedMap).universally f ↔ (topologically @IsClosedMap).universally f
Tactic: rw [universallyClosed_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
⊢ UniversallyClosed f
have rw : (topologically @IsClosedMap).universally f
Tactic: rw [universallyClosed_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
hf : IsPullback f' i₁ i₂ f
⊢ topologically (@IsClosedMap) f'
have hf' : IsClosedImmersion f'
Tactic: have hf' : IsClosedImmersion f' :=
    MorphismProperty.of_isPullback hf.flip inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderComposition @UniversallyClosed
have rw : (topologically @IsClosedMap).universally.IsStableUnderComposition
Tactic: rw [universallyClosed_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : UniversallyClosed (f ≫ g)
inst_1 : Surjective f
⊢ UniversallyClosed g
have universally_isClosedMap : (topologically @IsClosedMap).universally g
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : UniversallyClosed (f ≫ g)
inst_1 : Surjective f
X' Y' : Scheme
i₁ : X' ⟶ Y
i₂ : Y' ⟶ Z
f' : X' ⟶ Y'
H : IsPullback f' i₁ i₂ g
⊢ topologically (@IsClosedMap) f'
have this : topologically @IsClosedMap (X := pullback i₁ f) (pullback.fst i₁ f ≫ f')
Tactic: have := UniversallyClosed.universally_isClosedMap _ _ _
    ((IsPullback.of_hasPullback i₁ f).paste_horiz H)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget @UniversallyClosed
have rw : IsZariskiLocalAtTarget.{u_1} (topologically @IsClosedMap).universally
Tactic: rw [universallyClosed_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget.{u_1} (topologically @IsClosedMap).universally
have hP₂ : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) {ι : Type u_1} (U : ι → Y.Opens),
  IsOpenCover U →
    (∀ (i : ι), topologically @IsClosedMap (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → topologically (@IsClosedMap) f
Tactic: apply universally_isZariskiLocalAtTarget
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → Y.Opens
hU : IsOpenCover U
H : ∀ (i : ι), topologically @IsClosedMap (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)
⊢ topologically (@IsClosedMap) f
have H₁ : ∀ (i : ι), IsClosedMap (X := ↥(↑(f ⁻¹ᵁ U i) : Scheme)) ((U i).carrier.restrictPreimage ⇑f)
Tactic: simp_rw [topologically, morphismRestrict_base] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
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))ᶜ
⊢ IsClosed Z
have simp : IsOpen.{u} (X := ↥(pullback f q)) (⋃ (i : 𝒰.I₀), ⇑fT ⁻¹' (↑(Ti i) : Set ↥T) ∩ ⇑p ⁻¹' (↑(U i) : Set ↥X))
Tactic: simp only [Z, isClosed_compl_iff, Opens.coe_iSup, Opens.coe_inf, Opens.map_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
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))ᶜ
⊢ CompactSpace.{u} ↥X
have hZ : IsClosed Z
Tactic: have hZ : IsClosed Z := by
    simp only [Z, isClosed_compl_iff, Opens.coe_iSup, Opens.coe_inf, Opens.map_coe]
    exact isOpen_iUnion fun i ↦ (fT.continuous.1 _ (Ti i).2).inter (p.continuous.1 _ (U i).2)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
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
⊢ CompactSpace.{u} ↥X
have ht : ∀ (i : 𝒰.I₀), t ∈ Ti i
Tactic: have ht (i : 𝒰.I₀) : t ∈ Ti i := show ψ (.X i) ≠ 0 by simp [ψ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
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
⊢ False
have suffices : ∃ (i : 𝒰.I₀), Membership.mem (α := ↥T) (Ti i) (fT z : ↥T) ∧ Membership.mem (α := ↥X) (U i) (p z : ↥X)
Tactic: suffices ∃ i, fT z ∈ Ti i ∧ p z ∈ U i from hz (by simpa)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
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
⊢ CompactSpace.{u} ↥X
have htZc : 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)⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
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
⊢ CompactSpace.{u} ↥X
have 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
Tactic: obtain ⟨U', ⟨g, rfl⟩, htU', hU'le⟩ := Opens.isBasis_iff_nbhd.mp isBasis_basic_opens htZc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
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
⊢ CompactSpace.{u} ↥X
have ht'g : 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'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (hypothesis)
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'
⊢ CompactSpace.{u} ↥X
have h : t' ∉ ⇑fT '' Z
Tactic: have h : t' ∉ fT '' Z := hU'le ht'g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
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
⊢ CompactSpace.{u} ↥X
have suffices : Eq.{u + 1} (α := Set ↥X) (⋃ i ∈ σ, (U i).carrier) Set.univ
Tactic: suffices ⋃ i ∈ σ, (U i).1 = Set.univ from
    ⟨this ▸ Finset.isCompact_biUnion _ fun i _ ↦ isCompact_range (𝒰.f i).continuous⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed (goal)
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
⊢ Eq.{u + 1} (α := Set ↥X) (⋃ i ∈ σ, (U i).carrier) Set.univ
have rw : ∀ (a : ↥X), ∃ (i : 𝒰.I₀) (_ : i ∈ σ), a ∈ (U i).carrier
Tactic: rw [Set.iUnion₂_eq_univ_iff]