awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
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 : α)
⊢ (U i).carrier.restrictPreimage f a = Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi

Tactic:
rw [closure_subtype] at ha

Premises used: closure_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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
⊢ Membership.mem (γ := Set α) (closure[inst] {x}) (↑a : α)

Tactic:
simp only [Opens.carrier_eq_coe, Set.image_singleton] at ha

Premises used: Set.image_singleton, TopologicalSpace.Opens.carrier_eq_coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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 : α)
⊢ (↑((U i).carrier.restrictPreimage f a) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ U i) y hi) : β)

Tactic:
apply_fun Subtype.val at hay

Premises used: Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
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] {x}) (↑a : α)
hay : f (↑a : α) = y
w : α
left : Membership.mem (γ := Set α) (closure[inst] {x}) (↑a : α)
right : f (↑a : α) = y
⊢ y ∈ f '' closure[inst] {x}

Tactic:
use a.val, ha, hay

Premises used: Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap).RespectsIso

Tactic:
topologically_respectsIso _ (fun f ↦ f.isOpenEmbedding.generalizingMap
    f.isOpenEmbedding.isOpen_range.stableUnderGeneralization) (fun _ _ hf hg ↦ hf.comp hg)

Premises used: Topology.IsOpenEmbedding.toIsEmbedding, GeneralizingMap.comp, Topology.IsInducing.generalizingMap, Topology.IsOpenEmbedding.isOpen_range, AlgebraicGeometry.topologically_respectsIso, Homeomorph.isOpenEmbedding, Topology.IsEmbedding.toIsInducing, IsOpen.stableUnderGeneralization
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtSource.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)

Tactic:
topologically_isZariskiLocalAtSource' (fun _ ↦ _) fun _ _ _ hU _ ↦ hU.generalizingMap_iff_comp

Premises used: TopologicalSpace.IsOpenCover.generalizingMap_iff_comp, AlgebraicGeometry.topologically_isZariskiLocalAtSource'
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Goal:
⊢ IsZariskiLocalAtTarget.{u_1}
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)

Tactic:
topologically_isZariskiLocalAtTarget' (fun _ ↦ _) fun _ _ _ hU _ ↦
    hU.generalizingMap_iff_restrictPreimage

Premises used: AlgebraicGeometry.topologically_isZariskiLocalAtTarget', TopologicalSpace.IsOpenCover.generalizingMap_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
UniversallyClosed.universally_isClosedMap _ _ _ IsPullback.of_id_snd

Premises used: CategoryTheory.IsPullback.of_id_snd, AlgebraicGeometry.topologically, AlgebraicGeometry.UniversallyClosed.universally_isClosedMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y), UniversallyClosed f ↔ (topologically @IsClosedMap).universally f
⊢ @UniversallyClosed = (topologically @IsClosedMap).universally

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
h h₁ : (topologically @IsClosedMap).universally f ↔ (topologically @IsClosedMap).universally f
⊢ UniversallyClosed f ↔ (topologically @IsClosedMap).universally f

Tactic:
rw [universallyClosed_iff]

Premises used: AlgebraicGeometry.universallyClosed_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsClosedImmersion f
rw : (topologically @IsClosedMap).universally f
⊢ UniversallyClosed f

Tactic:
rw [universallyClosed_eq]

Premises used: AlgebraicGeometry.universallyClosed_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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
⊢ IsClosedImmersion f'

Tactic:
have hf' : IsClosedImmersion f' :=
    MorphismProperty.of_isPullback hf.flip inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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
hf' : IsClosedImmersion f'
⊢ topologically (@IsClosedMap) f'

Tactic:
f'.isClosedEmbedding.isClosedMap

Premises used: Topology.IsClosedEmbedding.isClosedMap, AlgebraicGeometry.topologically, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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
hf' : IsClosedImmersion f'
⊢ topologically (@IsClosedMap) f'

Tactic:
exact f'.isClosedEmbedding.isClosedMap

Premises used: Topology.IsClosedEmbedding.isClosedMap, AlgebraicGeometry.Scheme.Hom.isClosedEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
⊢ RespectsIso @UniversallyClosed

Tactic:
universallyClosed_eq.symm ▸ universally_respectsIso (topologically @IsClosedMap)

Premises used: Eq.rec, IsClosedMap, AlgebraicGeometry.topologically, CategoryTheory.MorphismProperty.universally_respectsIso, Eq.symm, AlgebraicGeometry.universallyClosed_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderBaseChange @UniversallyClosed

Tactic:
universallyClosed_eq.symm ▸ universally_isStableUnderBaseChange (topologically @IsClosedMap)

Premises used: Eq.rec, IsClosedMap, AlgebraicGeometry.topologically, CategoryTheory.MorphismProperty.universally_isStableUnderBaseChange, Eq.symm, AlgebraicGeometry.universallyClosed_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
rw : (topologically @IsClosedMap).universally.IsStableUnderComposition
⊢ IsStableUnderComposition @UniversallyClosed

Tactic:
rw [universallyClosed_eq]

Premises used: AlgebraicGeometry.universallyClosed_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsClosedMap).universally.IsStableUnderComposition

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : UniversallyClosed (f ≫ g)
inst_1 : Surjective f
universally_isClosedMap : (topologically @IsClosedMap).universally g
⊢ UniversallyClosed g

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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 (X := pullback i₁ f) (pullback.fst i₁ f ≫ f')

Tactic:
have := UniversallyClosed.universally_isClosedMap _ _ _
    ((IsPullback.of_hasPullback i₁ f).paste_horiz H)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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
this : topologically @IsClosedMap (X := pullback i₁ f) (pullback.fst i₁ f ≫ f')
⊢ topologically (@IsClosedMap) f'

Tactic:
IsClosedMap.of_comp_surjective (MorphismProperty.pullback_fst (P := @Surjective) _ _ ‹_›).1
    (Scheme.Hom.continuous _) this

Premises used: IsClosedMap.of_comp_surjective, AlgebraicGeometry.topologically, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Surjective.surj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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
this : topologically @IsClosedMap (X := pullback i₁ f) (pullback.fst i₁ f ≫ f')
⊢ topologically (@IsClosedMap) f'

Tactic:
exact IsClosedMap.of_comp_surjective (MorphismProperty.pullback_fst (P := @Surjective) _ _ ‹_›).1
    (Scheme.Hom.continuous _) this

Premises used: IsClosedMap.of_comp_surjective, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Surjective.surj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : UniversallyClosed f
hg : UniversallyClosed g
⊢ UniversallyClosed (f ≫ g)

Tactic:
comp_mem _ _ _ hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
hg : UniversallyClosed g
⊢ UniversallyClosed (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g hg

Premises used: CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
hf : UniversallyClosed f
⊢ UniversallyClosed (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g hf

Premises used: CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsZariskiLocalAtTarget.{u_1} (topologically @IsClosedMap).universally
⊢ IsZariskiLocalAtTarget @UniversallyClosed

Tactic:
rw [universallyClosed_eq]

Premises used: AlgebraicGeometry.universallyClosed_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
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
⊢ IsZariskiLocalAtTarget.{u_1} (topologically @IsClosedMap).universally

Tactic:
apply universally_isZariskiLocalAtTarget

Premises used: AlgebraicGeometry.universally_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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)
⊢ ∀ (i : ι), IsClosedMap (X := ↥(↑(f ⁻¹ᵁ U i) : Scheme)) ((U i).carrier.restrictPreimage ⇑f)

Tactic:
simp_rw [topologically, morphismRestrict_base] at H

Premises used: AlgebraicGeometry.morphismRestrict_base, AlgebraicGeometry.topologically
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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 : ι), IsClosedMap (X := ↥(↑(f ⁻¹ᵁ U i) : Scheme)) ((U i).carrier.restrictPreimage ⇑f)
⊢ topologically (@IsClosedMap) f

Tactic:
hU.isClosedMap_iff_restrictPreimage.mpr H

Premises used: Iff.mpr, AlgebraicGeometry.topologically, TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
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 : ι), IsClosedMap (X := ↥(↑(f ⁻¹ᵁ U i) : Scheme)) ((U i).carrier.restrictPreimage ⇑f)
⊢ topologically (@IsClosedMap) f

Tactic:
exact hU.isClosedMap_iff_restrictPreimage.mpr H

Premises used: Iff.mpr, TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f_1 f : X ⟶ Y
V : Y.Opens
inst : UniversallyClosed f
⊢ UniversallyClosed (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- 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))ᶜ
simp : IsOpen.{u} (X := ↥(pullback f q)) (⋃ (i : 𝒰.I₀), ⇑fT ⁻¹' (↑(Ti i) : Set ↥T) ∩ ⇑p ⁻¹' (↑(U i) : Set ↥X))
⊢ IsClosed Z

Tactic:
simp only [Z, isClosed_compl_iff, Opens.coe_iSup, Opens.coe_inf, Opens.map_coe]

Premises used: TopologicalSpace.Opens.map_coe, TopologicalSpace.Opens.coe_iSup, TopologicalSpace.Opens.coe_inf, isClosed_compl_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))ᶜ
⊢ IsOpen.{u} (X := ↥(pullback f q)) (⋃ (i : 𝒰.I₀), ⇑fT ⁻¹' (↑(Ti i) : Set ↥T) ∩ ⇑p ⁻¹' (↑(U i) : Set ↥X))

Tactic:
isOpen_iUnion fun i ↦ (fT.continuous.1 _ (Ti i).2).inter (p.continuous.1 _ (U i).2)

Premises used: TopologicalSpace.Opens.carrier, SetLike.coe, isOpen_iUnion, IsOpen.inter, AlgebraicGeometry.Scheme.Hom.continuous, TopologicalSpace.Opens.is_open', Continuous.isOpen_preimage
-- 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))ᶜ
⊢ IsOpen.{u} (X := ↥(pullback f q)) (⋃ (i : 𝒰.I₀), ⇑fT ⁻¹' (↑(Ti i) : Set ↥T) ∩ ⇑p ⁻¹' (↑(U i) : Set ↥X))

Tactic:
exact isOpen_iUnion fun i ↦ (fT.continuous.1 _ (Ti i).2).inter (p.continuous.1 _ (U i).2)

Premises used: TopologicalSpace.Opens.carrier, isOpen_iUnion, IsOpen.inter, AlgebraicGeometry.Scheme.Hom.continuous, TopologicalSpace.Opens.is_open', Continuous.isOpen_preimage
-- 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))ᶜ
⊢ 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)
-- 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
i : 𝒰.I₀
⊢ Ne (α := K) ((ψ : (a : MvPolynomial 𝒰.I₀ K) → K) (MvPolynomial.X i) : K) (0 : K)

Tactic:
simp [ψ]
-- 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
⊢ ∀ (i : 𝒰.I₀), t ∈ Ti i

Tactic:
have ht (i : 𝒰.I₀) : t ∈ Ti i := show ψ (.X i) ≠ 0 by simp [ψ]
-- 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
this : ∃ (i : 𝒰.I₀), Membership.mem (α := ↥T) (Ti i) (fT z : ↥T) ∧ Membership.mem (α := ↥X) (U i) (p z : ↥X)
⊢ z ∈ (↑(⨆ (i : 𝒰.I₀), fT ⁻¹ᵁ Ti i ⊓ p ⁻¹ᵁ U i) : Set ↥(pullback f q))

Tactic:
simpa
-- 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
suffices : ∃ (i : 𝒰.I₀), Membership.mem (α := ↥T) (Ti i) (fT z : ↥T) ∧ Membership.mem (α := ↥X) (U i) (p z : ↥X)
⊢ False

Tactic:
suffices ∃ i, fT z ∈ Ti i ∧ p z ∈ U i from hz (by simpa)