awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).toAlgebra
apply :
  Algebra.HasGoingDown.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
    (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))))

Tactic:
apply Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp

Premises used: Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).toAlgebra
⊢ Algebra.HasGoingDown.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
    (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)

Tactic:
Algebra.HasGoingDown.of_flat

Premises used: Algebra.HasGoingDown.of_flat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).toAlgebra
convert_6 :
  Module.Flat.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
    (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)
⊢ Algebra.HasGoingDown.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
    (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)

Tactic:
convert! Algebra.HasGoingDown.of_flat

Premises used: Algebra.HasGoingDown.of_flat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).toAlgebra
⊢ Module.Flat.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
    (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)

Tactic:
HasRingHomProperty.appLE @Flat f ‹_› U V e

Premises used: AlgebraicGeometry.Flat, RingHom.Flat, AlgebraicGeometry.HasRingHomProperty.appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
this :
  HasRingHomProperty.{u} (topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
U : (↑Y.affineOpens : Type u)
V : (↑X.affineOpens : Type u)
e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)
algInst : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).toAlgebra
⊢ Module.Flat.{u, u} (↑(CommRingCat.of (↑Γ(Y, (↑U : Y.Opens)) : Type u)) : Type u)
    (↑(CommRingCat.of (↑Γ(X, (↑V : X.Opens)) : Type u)) : Type u)

Tactic:
exact HasRingHomProperty.appLE @Flat f ‹_› U V e

Premises used: AlgebraicGeometry.Flat, AlgebraicGeometry.HasRingHomProperty.appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
⊢ UniversallyOpen f

Tactic:
⟨universally_mk' _ _ fun _ _ ↦ isOpenMap_of_generalizingMap _ (Flat.generalizingMap _)⟩

Premises used: CategoryTheory.MorphismProperty.universally_mk', AlgebraicGeometry.UniversallyOpen.mk, AlgebraicGeometry.isOpenMap_of_generalizingMap, AlgebraicGeometry.Flat.generalizingMap, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
inr :
  ∀ (this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f
wlog : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f
⊢ UniversallyOpen f

Tactic:
wlog hX : ∃ S, X = Spec S generalizing X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ UniversallyOpen f

Tactic:
(IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ UniversallyOpen f

Tactic:
refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ this _ ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
X : Scheme
f : X ⟶ Y
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Y), UniversallyOpen f
⊢ UniversallyOpen f

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
S : CommRingCat
f : Spec S ⟶ Y
inr :
  ∀
    (this :
      ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
        (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f)
    (hY : ¬∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
wlog :
  ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
    (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
⊢ UniversallyOpen f

Tactic:
wlog hY : ∃ K, Y = Spec K ∧ IsField K generalizing Y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
    (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
hY : ¬∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)
⊢ Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))

Tactic:
have inst : Subsingleton (Spec Γ(Y, ⊤)) := Y.isoSpec.inv.homeomorph.subsingleton
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
Y : Scheme
inst_1 : IsIntegral Y
inst_2 : Subsingleton.{u + 1} ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
    (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
hY : ¬∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)
inst : Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))
⊢ UniversallyOpen f

Tactic:
(MorphismProperty.cancel_right_of_respectsIso _ _ Y.isoSpec.hom).mp
      (this _ ⟨_, rfl, isField_of_isIntegral_of_subsingleton _⟩)

Premises used: AlgebraicGeometry.Scheme.isoSpec, And.intro, Exists.intro, Iff.mp, CategoryTheory.Iso.hom, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, rfl, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
Y : Scheme
inst_1 : IsIntegral Y
inst_2 : Subsingleton.{u + 1} ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
    (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
hY : ¬∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)
inst : Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))
⊢ UniversallyOpen f

Tactic:
exact (MorphismProperty.cancel_right_of_respectsIso _ _ Y.isoSpec.hom).mp
      (this _ ⟨_, rfl, isField_of_isIntegral_of_subsingleton _⟩)

Premises used: AlgebraicGeometry.Scheme.isoSpec, And.intro, Exists.intro, Iff.mp, CategoryTheory.Iso.hom, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton, rfl, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
S : CommRingCat
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
f : Spec S ⟶ Y
hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)
obtain :
  ∀ (K : CommRingCat.{u}) (hK : IsField.{u} (↑K : Type u)) [IsIntegral.{u} (Spec K)] [Subsingleton.{u + 1} ↥(Spec K)]
    (f : Spec S ⟶ Spec K), UniversallyOpen f
⊢ UniversallyOpen f

Tactic:
obtain ⟨K, rfl, hK⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
f : Spec S ⟶ Spec K
obtain : ∀ (φ : K ⟶ S), UniversallyOpen (Spec.map φ)
⊢ UniversallyOpen f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
⊢ UniversallyOpen (Spec.map φ)

Tactic:
⟨universally_mk' _ _ fun {T} g _ ↦ ?_⟩

Premises used: CategoryTheory.MorphismProperty.universally_mk', AlgebraicGeometry.UniversallyOpen.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
refine :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
⊢ UniversallyOpen (Spec.map φ)

Tactic:
refine ⟨universally_mk' _ _ fun {T} g _ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
inr :
  ∀
    (this :
      ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
        topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)))
    (hT : ¬∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
wlog :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))

Tactic:
wlog hT : ∃ R, T = Spec R generalizing T
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))

Tactic:
(IsZariskiLocalAtTarget.iff_of_openCover T.affineCover).mpr fun i ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
inr :
  ∀ (i : T.affineCover.toPreZeroHypercover.1),
    topologically @IsOpenMap (X :=
      PreZeroHypercover.X (S := pullback g (Spec.map φ))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
        i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
        PreZeroHypercover.X (S := pullback g (Spec.map φ))
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
            i ⟶
          T.affineCover.X i)
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))

Tactic:
refine (IsZariskiLocalAtTarget.iff_of_openCover T.affineCover).mpr fun i ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
i : T.affineCover.toPreZeroHypercover.1
⊢ topologically @IsOpenMap (X :=
    PreZeroHypercover.X (S := pullback g (Spec.map φ))
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
      PreZeroHypercover.X (S := pullback g (Spec.map φ))
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
          i ⟶
        T.affineCover.X i)

Tactic:
(MorphismProperty.cancel_left_of_respectsIso _
      ((pullbackRightPullbackFstIso ..).inv ≫ (pullbackSymmetry ..).hom) _).mp ?_

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Limits.limit, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
i : T.affineCover.toPreZeroHypercover.1
inr :
  topologically @IsOpenMap (X := pullback (T.affineCover.f i ≫ g) (Spec.map φ))
    (CategoryStruct.comp (Y :=
        pullback (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)) (T.affineCover.f i))
        (CategoryStruct.comp (Y :=
            pullback (Y := pullback g (Spec.map φ)) (T.affineCover.f i) (pullback.fst g (Spec.map φ)))
            (Iso.inv (pullbackRightPullbackFstIso g (Spec.map φ) (T.affineCover.f i)))
            (Iso.hom (pullbackSymmetry (T.affineCover.f i) (pullback.fst g (Spec.map φ)))) :
          pullback (T.affineCover.f i ≫ g) (Spec.map φ) ⟶
            pullback (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)) (T.affineCover.f i))
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
          PreZeroHypercover.X (S := pullback g (Spec.map φ))
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
              i ⟶
            T.affineCover.X i) :
      pullback (T.affineCover.f i ≫ g) (Spec.map φ) ⟶ T.affineCover.X i)
⊢ topologically @IsOpenMap (X :=
    PreZeroHypercover.X (S := pullback g (Spec.map φ))
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
      PreZeroHypercover.X (S := pullback g (Spec.map φ))
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
          i ⟶
        T.affineCover.X i)

Tactic:
refine (MorphismProperty.cancel_left_of_respectsIso _
      ((pullbackRightPullbackFstIso ..).inv ≫ (pullbackSymmetry ..).hom) _).mp ?_

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.CategoryStruct.comp, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
i : T.affineCover.toPreZeroHypercover.1
⊢ topologically @IsOpenMap (X := pullback (T.affineCover.f i ≫ g) (Spec.map φ))
    (CategoryStruct.comp (Y :=
        pullback (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)) (T.affineCover.f i))
        (CategoryStruct.comp (Y :=
            pullback (Y := pullback g (Spec.map φ)) (T.affineCover.f i) (pullback.fst g (Spec.map φ)))
            (Iso.inv (pullbackRightPullbackFstIso g (Spec.map φ) (T.affineCover.f i)))
            (Iso.hom (pullbackSymmetry (T.affineCover.f i) (pullback.fst g (Spec.map φ)))) :
          pullback (T.affineCover.f i ≫ g) (Spec.map φ) ⟶
            pullback (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)) (T.affineCover.f i))
        (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
          PreZeroHypercover.X (S := pullback g (Spec.map φ))
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
              i ⟶
            T.affineCover.X i) :
      pullback (T.affineCover.f i ≫ g) (Spec.map φ) ⟶ T.affineCover.X i)

Tactic:
simpa [Scheme.Cover.pullbackHom] using this _ _ ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
hT : ∃ (R : CommRingCat.{u}), T = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))

Tactic:
obtain ⟨R, rfl⟩ := hT

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
g : Spec R ⟶ Spec K
h : HasPullback g (Spec.map φ)
obtain :
  ∀ (ψ : K ⟶ R) (x : HasPullback (Spec.map ψ) (Spec.map φ)),
    topologically @IsOpenMap (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))

Tactic:
obtain ⟨ψ, rfl⟩ := Spec.map_surjective g

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl