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

Tactic:
rw [comap_basicOpen, show φ (.X i) = 0 by simpa [φ] using (hx i · hi₂), basicOpen_zero] at hi₁

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

Tactic:
rw [comap_basicOpen, show φ (.X i) = 0 by simpa [φ] using (hx i · hi₂), basicOpen_zero] at hi₁

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

Tactic:
cases hi₁
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
rw :
  Continuous (X := ↥X) (Y := ↥Y) ⇑f ∧
    IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ∧ ∀ (y : ↥Y), IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
⊢ IsProperMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
rw [isProperMap_iff_isClosedMap_and_compact_fibers]

Premises used: isProperMap_iff_isClosedMap_and_compact_fibers
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
⊢ Continuous (X := ↥X) (Y := ↥Y) ⇑f ∧
    IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ∧ ∀ (y : ↥Y), IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})

Tactic:
⟨f.continuous, f.isClosedMap, fun y ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.isClosedMap, And.intro, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
refine : ∀ (y : ↥Y), IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})
⊢ Continuous (X := ↥X) (Y := ↥Y) ⇑f ∧
    IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ∧ ∀ (y : ↥Y), IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})

Tactic:
refine ⟨f.continuous, f.isClosedMap, fun y ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
y : ↥Y
⊢ CompactSpace.{u} ↥(pullback f (Y.fromSpecResidueField y))

Tactic:
have := compactSpace_of_universallyClosed (pullback.snd f (Y.fromSpecResidueField y))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
y : ↥Y
this : CompactSpace.{u} ↥(pullback f (Y.fromSpecResidueField y))
rw :
  IsCompact (X := ↥X)
    (Set.range (ι := ↥(pullback f (Y.fromSpecResidueField y))) ⇑(pullback.fst f (Y.fromSpecResidueField y)))
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) ⇑f {y})

Tactic:
rw [← Scheme.range_fromSpecResidueField, ← Scheme.Pullback.range_fst]

Premises used: AlgebraicGeometry.Scheme.Pullback.range_fst, AlgebraicGeometry.Scheme.range_fromSpecResidueField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
y : ↥Y
this : CompactSpace.{u} ↥(pullback f (Y.fromSpecResidueField y))
⊢ IsCompact (X := ↥X)
    (Set.range (ι := ↥(pullback f (Y.fromSpecResidueField y))) ⇑(pullback.fst f (Y.fromSpecResidueField y)))

Tactic:
isCompact_range (Scheme.Hom.continuous _)

Premises used: isCompact_range, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
y : ↥Y
this : CompactSpace.{u} ↥(pullback f (Y.fromSpecResidueField y))
⊢ IsCompact (X := ↥X)
    (Set.range (ι := ↥(pullback f (Y.fromSpecResidueField y))) ⇑(pullback.fst f (Y.fromSpecResidueField y)))

Tactic:
exact isCompact_range (Scheme.Hom.continuous _)

Premises used: isCompact_range, AlgebraicGeometry.Scheme.Hom.continuous
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
rw : @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally
⊢ @UniversallyClosed = (topologically @SpecializingMap).universally ⊓ @QuasiCompact

Tactic:
rw [← universally_eq_iff (P := @QuasiCompact).mpr inferInstance, ← universally_inf]

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.universally_inf, inferInstance, CategoryTheory.MorphismProperty.universally_eq_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
a : @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
a₁ : (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed
⊢ @UniversallyClosed = (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
a : universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally
⊢ @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
rw [← universally_eq_iff (P := @UniversallyClosed).mpr inferInstance]

Premises used: Iff.mpr, inferInstance, CategoryTheory.MorphismProperty.universally_eq_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
universally_mono fun X Y f H ↦ ⟨f.isClosedMap.specializingMap, inferInstance⟩

Premises used: AlgebraicGeometry.Scheme.Hom.isClosedMap, inferInstance, And.intro, IsClosedMap.specializingMap, CategoryTheory.MorphismProperty.universally_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
⊢ universally @UniversallyClosed ≤ (topologically @SpecializingMap ⊓ @QuasiCompact).universally

Tactic:
exact universally_mono fun X Y f H ↦ ⟨f.isClosedMap.specializingMap, inferInstance⟩

Premises used: CategoryTheory.MorphismProperty.universally_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
a : (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ @UniversallyClosed

Tactic:
rw [universallyClosed_eq]

Premises used: AlgebraicGeometry.universallyClosed_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally

Tactic:
universally_mono fun X Y f ⟨h₁, h₂⟩ ↦ (isClosedMap_iff_specializingMap _).mpr h₁

Premises used: Iff.mpr, IsClosedMap, AlgebraicGeometry.topologically, _private.0.AlgebraicGeometry.universallyClosed_eq_universallySpecializing.match_1, CategoryTheory.MorphismProperty.universally_mono, AlgebraicGeometry.isClosedMap_iff_specializingMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
⊢ (topologically @SpecializingMap ⊓ @QuasiCompact).universally ≤ (topologically @IsClosedMap).universally

Tactic:
exact universally_mono fun X Y f ⟨h₁, h₂⟩ ↦ (isClosedMap_iff_specializingMap _).mpr h₁

Premises used: CategoryTheory.MorphismProperty.universally_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyClosed f
inst_1 : IsDominant f
rw : Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
rw₁ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) Set.univ
rw₂ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (closure (Set.range (ι := ↥X) ⇑f))
rw₃ rw₄ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥X) ⇑f)
⊢ Surjective f

Tactic:
rw [surjective_iff, ← Set.range_eq_univ, ← f.denseRange.closure_range,
    f.isClosedMap.isClosed_range.closure_eq]

Premises used: Set.range_eq_univ, AlgebraicGeometry.Scheme.Hom.denseRange, IsClosed.closure_eq, AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.surjective_iff, DenseRange.closure_range, IsClosedMap.isClosed_range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyInjective f
⊢ Injective (α := ↥X) (β := ↥Y) ⇑f

Tactic:
UniversallyInjective.universally_injective _ _ _ .of_id_snd

Premises used: CategoryTheory.IsPullback.of_id_snd, AlgebraicGeometry.topologically, AlgebraicGeometry.UniversallyInjective.universally_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
h :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y),
    UniversallyInjective f ↔
      (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦
            Injective x).universally
        f
⊢ @UniversallyInjective =
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
h h₁ :
  (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
      f ↔
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
      f
⊢ UniversallyInjective f ↔
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
      f

Tactic:
rw [universallyInjective_iff]

Premises used: AlgebraicGeometry.universallyInjective_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
a : @UniversallyInjective ≤ diagonal @Surjective
a₁ : diagonal @Surjective ≤ @UniversallyInjective
⊢ @UniversallyInjective = diagonal @Surjective

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
⊢ diagonal (@Surjective) f

Tactic:
⟨fun x ↦ ⟨pullback.fst f f x, hf.1 _ _ _ (IsPullback.of_hasPullback f f) ?_⟩⟩

Premises used: CategoryTheory.MorphismProperty.diagonal, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Limits.pullback.fst, AlgebraicGeometry.Surjective.mk, Exists.intro, CategoryTheory.IsPullback.of_hasPullback, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.UniversallyInjective.universally_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
a :
  ∀ (x : ↥(pullback.diagonalObj f)),
    Eq (α := ↥X)
      ((pullback.fst f f) ((pullback.diagonal f) ((pullback.fst f f) x : ↥X) : ↥(pullback.diagonalObj f)) : ↥X)
      ((pullback.fst f f) x : ↥X)
⊢ diagonal (@Surjective) f

Tactic:
refine ⟨fun x ↦ ⟨pullback.fst f f x, hf.1 _ _ _ (IsPullback.of_hasPullback f f) ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↥(pullback.diagonalObj f)
a : Eq (α := ↥X) ((𝟙 X) ((pullback.fst f f) x : ↥X) : ↥X) ((pullback.fst f f) x : ↥X)
⊢ Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) ((pullback.fst f f) x : ↥X) : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.fst f f) x : ↥X)

Tactic:
rw [← Scheme.Hom.comp_apply, pullback.diagonal_fst]

Premises used: CategoryTheory.Limits.pullback.diagonal_fst, AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
hf : UniversallyInjective f
x : ↥(pullback.diagonalObj f)
⊢ Eq (α := ↥X) ((𝟙 X) ((pullback.fst f f) x : ↥X) : ↥X) ((pullback.fst f f) x : ↥X)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
a :
  (diagonal @Surjective).universally ≤
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally
⊢ diagonal @Surjective ≤ @UniversallyInjective

Tactic:
rw [← universally_eq_iff.mpr (inferInstance : IsStableUnderBaseChange (diagonal @Surjective)),
      universallyInjective_eq]

Premises used: Iff.mpr, AlgebraicGeometry.universallyInjective_eq, inferInstance, CategoryTheory.MorphismProperty.universally_eq_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
a :
  diagonal @Surjective ≤
    topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x
⊢ (diagonal @Surjective).universally ≤
    (topologically fun {α β : Type u_1} [TopologicalSpace α] [TopologicalSpace β] (x : α → β) ↦ Injective x).universally

Tactic:
apply universally_mono

Premises used: CategoryTheory.MorphismProperty.universally_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
a : ∀ (t : ↥(pullback f f)) (ht₁ : (pullback.fst f f) t = x₁) (ht₂ : (pullback.snd f f) t = x₂), x₁ = x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨t, ht₁, ht₂⟩ := Scheme.Pullback.exists_preimage_pullback _ _ e

Premises used: AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥(pullback f f)
ht₁ : (pullback.fst f f) t = x₁
ht₂ : (pullback.snd f f) t = x₂
a :
  ∀ (t : ↥X) (ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁)
    (ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂), x₁ = x₂
⊢ x₁ = x₂

Tactic:
obtain ⟨t, rfl⟩ := hf.1 t

Premises used: AlgebraicGeometry.Surjective.surj, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
hf : diagonal (@Surjective) f
x₁ x₂ : ↥X
e : Eq (α := ↥Y) (f x₁ : ↥Y) (f x₂ : ↥Y)
t : ↥X
ht₁ : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₁
ht₂ : (pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a : (pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) = x₂
a₁ :
  Eq (α := ↥X) ((pullback.fst f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
a₂ :
  Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
    ((pullback.snd f f) ((pullback.diagonal f) t : ↥(pullback.diagonalObj f)) : ↥X)
a₃ :
  Eq (α := ↥X) ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.fst f f)) t : ↥X)
    ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.snd f f)) t : ↥X)
a₄ :
  Eq (α := ↥X) ((𝟙 X) t : ↥X)
    ((CategoryStruct.comp (Y := pullback f f) (pullback.diagonal f) (pullback.snd f f)) t : ↥X)
a₅ a₆ : Eq (α := ↥X) ((𝟙 X) t : ↥X) ((𝟙 X) t : ↥X)
⊢ x₁ = x₂

Tactic:
rw [← ht₁, ← ht₂, ← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, pullback.diagonal_fst,
      pullback.diagonal_snd]

Premises used: CategoryTheory.Limits.pullback.diagonal_snd, CategoryTheory.Limits.pullback.diagonal_fst, AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
rw : diagonal (@Surjective) f ↔ Surjective (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ UniversallyInjective f ↔ Surjective (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
rw [universallyInjective_eq_diagonal]

Premises used: AlgebraicGeometry.universallyInjective_eq_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ diagonal (@Surjective) f ↔ Surjective (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Mono f
⊢ UniversallyInjective f

Tactic:
have := (pullback.isIso_diagonal_iff f).mpr inferInstance
  (UniversallyInjective.iff_diagonal f).mpr inferInstance

Premises used: Iff.mpr, AlgebraicGeometry.UniversallyInjective.iff_diagonal, inferInstance, CategoryTheory.Limits.pullback.isIso_diagonal_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
⊢ RespectsIso @UniversallyInjective

Tactic:
universallyInjective_eq_diagonal.symm ▸ inferInstance

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

Tactic:
universallyInjective_eq_diagonal.symm ▸ inferInstance

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.universallyInjective_eq_diagonal, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsStableUnderComposition @UniversallyInjective

Tactic:
universallyInjective_eq ▸ inferInstance

Premises used: AlgebraicGeometry.universallyInjective_eq, Eq.rec, inferInstance, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget @UniversallyInjective

Tactic:
universallyInjective_eq_diagonal.symm ▸ inferInstance

Premises used: Eq.rec, inferInstance, AlgebraicGeometry.universallyInjective_eq_diagonal, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : UniversallyOpen f
⊢ IsOpenMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
UniversallyOpen.universally_isOpenMap _ _ _ IsPullback.of_id_snd

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

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

Tactic:
rw [universallyOpen_iff]

Premises used: AlgebraicGeometry.universallyOpen_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
rw : (topologically @IsOpenMap).universally f
⊢ UniversallyOpen f

Tactic:
rw [eq]

Premises used: AlgebraicGeometry.UniversallyOpen.eq
-- 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
⊢ IsOpenImmersion f'

Tactic:
have hf' : IsOpenImmersion f' := MorphismProperty.of_isPullback hf.flip inferInstance