awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
hf : IsPullback f' i₁ i₂ f
hf' : IsOpenImmersion f'
⊢ topologically (@IsOpenMap) f'

Tactic:
f'.isOpenEmbedding.isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.topologically, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
X' Y' : Scheme
i₁ : X' ⟶ X
i₂ : Y' ⟶ Y
f' : X' ⟶ Y'
hf : IsPullback f' i₁ i₂ f
hf' : IsOpenImmersion f'
⊢ topologically (@IsOpenMap) f'

Tactic:
exact f'.isOpenEmbedding.isOpenMap

Premises used: Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ RespectsIso @UniversallyOpen

Tactic:
eq.symm ▸ inferInstance

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.UniversallyOpen.eq, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderBaseChange @UniversallyOpen

Tactic:
eq.symm ▸ inferInstance

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.UniversallyOpen.eq, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
rw : (topologically @IsOpenMap).universally.IsStableUnderComposition
⊢ IsStableUnderComposition @UniversallyOpen

Tactic:
rw [eq]

Premises used: AlgebraicGeometry.UniversallyOpen.eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsOpenMap).universally.IsStableUnderComposition

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : UniversallyOpen f
hg : UniversallyOpen g
⊢ UniversallyOpen (f ≫ g)

Tactic:
comp_mem _ _ _ hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
hg : UniversallyOpen g
⊢ UniversallyOpen (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.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
hf : UniversallyOpen f
⊢ UniversallyOpen (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.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsZariskiLocalAtTarget.{u_1} (topologically @IsOpenMap).universally
⊢ IsZariskiLocalAtTarget @UniversallyOpen

Tactic:
rw [eq]

Premises used: AlgebraicGeometry.UniversallyOpen.eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
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 @IsOpenMap (X := (↑(f ⁻¹ᵁ U i) : Scheme)) (f ∣_ U i)) → topologically (@IsOpenMap) f
⊢ IsZariskiLocalAtTarget.{u_1} (topologically @IsOpenMap).universally

Tactic:
apply universally_isZariskiLocalAtTarget

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

Tactic:
hU.isOpenMap_iff_restrictPreimage.mpr H

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

Tactic:
exact hU.isOpenMap_iff_restrictPreimage.mpr H

Premises used: Iff.mpr, TopologicalSpace.IsOpenCover.isOpenMap_iff_restrictPreimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
rw : IsZariskiLocalAtSource.{u_1} (topologically @IsOpenMap).universally
⊢ IsZariskiLocalAtSource @UniversallyOpen

Tactic:
rw [eq]

Premises used: AlgebraicGeometry.UniversallyOpen.eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource.{u_1} (topologically @IsOpenMap).universally

Tactic:
universally_isZariskiLocalAtSource _

Premises used: AlgebraicGeometry.universally_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtSource.{u_1} (topologically @IsOpenMap).universally

Tactic:
exact universally_isZariskiLocalAtSource _

Premises used: AlgebraicGeometry.universally_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap (X :=
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically IsOpenMap) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap (X :=
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i))

Tactic:
this _ ?_ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
inr :
  GeneralizingMap (X := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) (Y := ↥(Y.affineCover.X i))
    ⇑(pullback.snd f (Y.affineCover.f i))
⊢ topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap (X :=
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i))

Tactic:
refine this _ ?_ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ GeneralizingMap (X := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) (Y := ↥(Y.affineCover.X i))
    ⇑(pullback.snd f (Y.affineCover.f i))

Tactic:
IsZariskiLocalAtTarget.of_isPullback (P := topologically GeneralizingMap)
      (iY := Y.affineCover.f i) (IsPullback.of_hasPullback ..) hf

Premises used: AlgebraicGeometry.topologically, AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ GeneralizingMap (X := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) (Y := ↥(Y.affineCover.X i))
    ⇑(pullback.snd f (Y.affineCover.f i))

Tactic:
exact IsZariskiLocalAtTarget.of_isPullback (P := topologically GeneralizingMap)
      (iY := Y.affineCover.f i) (IsPullback.of_hasPullback ..) hf

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥Y) ⇑f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f]
    (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
        [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
        topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inr :
  ∀ (i : X.affineCover.I₀),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := topologically IsOpenMap) X.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)

Tactic:
this f _ _ ?_ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
inr : GeneralizingMap (X := ↥(X.affineCover.X i)) (Y := ↥(Spec R)) ⇑(X.affineCover.f i ≫ f)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)

Tactic:
refine this f _ _ ?_ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
⊢ GeneralizingMap (X := ↥(X.affineCover.X i)) (Y := ↥(Spec R)) ⇑(X.affineCover.f i ≫ f)

Tactic:
IsZariskiLocalAtSource.comp (P := topologically GeneralizingMap) hf _

Premises used: AlgebraicGeometry.topologically, AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [LocallyOfFinitePresentation f] (hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
i : X.affineCover.I₀
⊢ GeneralizingMap (X := ↥(X.affineCover.X i)) (Y := ↥(Spec R)) ⇑(X.affineCover.f i ≫ f)

Tactic:
exact IsZariskiLocalAtSource.comp (P := topologically GeneralizingMap) hf _

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X_2 Y : Scheme
f_2 : X_2 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥X) (Y := ↥(Spec R)) ⇑f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [LocallyOfFinitePresentation f]
    (hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑f),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f_2 : X ⟶ Y
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : LocallyOfFinitePresentation f
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑f
obtain :
  ∀ (φ : R ⟶ S) [LocallyOfFinitePresentation (Spec.map φ)]
    (hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)),
    topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (Spec.map φ)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
⊢ IsOpenMap.{u, u} (X := PrimeSpectrum (↑S : Type u)) (Y := PrimeSpectrum (↑R : Type u))
    (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u)))

Tactic:
PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation

Premises used: PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
convert_6 : Algebra.HasGoingDown.{u, u} (↑R : Type u) (↑S : Type u)
convert_7 : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (Spec.map φ)

Tactic:
convert! PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation

Premises used: PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
convert_6 convert_6₁ convert_6₂ convert_6₃ :
  GeneralizingMap.{u, u} (X := PrimeSpectrum (↑S : Type u)) (Y := PrimeSpectrum (↑R : Type u))
    (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u)))
⊢ Algebra.HasGoingDown.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
rwa [Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap]

Premises used: Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap (X := ↥(Spec S)) (Y := ↥(Spec R)) ⇑(Spec.map φ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
⊢ Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
apply (HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)).mp inferInstance

Premises used: inferInstance, AlgebraicGeometry.HasRingHomProperty.Spec_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
⊢ 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))

Tactic:
have := HasRingHomProperty.of_isZariskiLocalAtSource_of_isZariskiLocalAtTarget.{u}
    (topologically GeneralizingMap)
-- 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))
rw :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    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))))
⊢ topologically (fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap) f

Tactic:
rw [HasRingHomProperty.iff_appLE (P := topologically GeneralizingMap)]

Premises used: AlgebraicGeometry.HasRingHomProperty.iff_appLE