awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
x : ↥X
hx : x ∈ U
y : (↑(X.presheaf.obj (op U)) : Type u_1)
hy :
  Eq (α := (↑(X.presheaf.stalk x) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        y :
      (↑(X.presheaf.stalk x) : Type u_1))
    ((CommRingCat.Hom.hom (X.presheaf.germ U x hx) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
        0 :
      (↑(X.presheaf.stalk x) : Type u_1))
W : Opens ↥X
hW : x ∈ W
iU : W ⟶ U
e :
  Eq (α := (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        y :
      (↑(X.presheaf.obj (op W)) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map iU.op) :
          (a : (↑(X.presheaf.obj (op U)) : Type u_1)) → (↑(X.presheaf.obj (op W)) : Type u_1))
        0 :
      (↑(X.presheaf.obj (op W)) : Type u_1))
this : Nonempty.{u_1 + 1} ↥(↑W : Scheme)
⊢ y = 0

Tactic:
exact map_injective_of_isIntegral X iU e

Premises used: AlgebraicGeometry.map_injective_of_isIntegral
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Function.Injective (α := (↑Γ(X, U) : Type u_1)) (β := (↑X.functionField : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Y := X.functionField) (X.germToFunctionField U)) :
      (a : (↑Γ(X, U) : Type u_1)) → (↑X.functionField : Type u_1))

Tactic:
germ_injective_of_isIntegral _ _ _

Premises used: AlgebraicGeometry.germ_injective_of_isIntegral
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
apply : IsGenericPoint (α := ↥Y) (f (genericPoint ↥X) : ↥Y) (Set.univ : Set ↥Y)
⊢ Eq (α := ↥Y) (f (genericPoint ↥X) : ↥Y) (genericPoint ↥Y : ↥Y)

Tactic:
apply ((genericPoint_spec Y).eq _).symm

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, genericPoint_spec, IsGenericPoint.eq, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Eq.symm, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ IsGenericPoint (α := ↥Y) (f (genericPoint ↥X) : ↥Y) (closure (Set.image (α := ↥X) (⇑f) Set.univ) : Set ↥Y)

Tactic:
(genericPoint_spec X).image f.continuous

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, IsGenericPoint.image, genericPoint_spec, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Eq (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
⊢ IsGenericPoint (α := ↥Y) (f (genericPoint ↥X) : ↥Y) (Set.univ : Set ↥Y)

Tactic:
convert! (genericPoint_spec X).image f.continuous

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, IsGenericPoint.image, genericPoint_spec, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Eq (α := Set ↥Y) (closure (Set.image (α := ↥X) (⇑f) Set.univ)) Set.univ
⊢ Eq (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))

Tactic:
symm
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Subset (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))
⊢ Eq (α := Set ↥Y) (closure (Set.image (α := ↥X) (⇑f) Set.univ)) Set.univ

Tactic:
rw [← Set.univ_subset_iff]

Premises used: Set.univ_subset_iff
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Subset (α := Set ↥Y) Set.univ (closure (Set.univ ∩ Set.range (ι := ↥X) ⇑f))

Tactic:
subset_closure_inter_of_isPreirreducible_of_isOpen _ f.isOpenEmbedding.isOpen_range _

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
h₁ : IsPreirreducible.{u_1} (X := ↥Y) Set.univ
h₂ : Set.Nonempty (α := ↥Y) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)
⊢ Subset (α := Set ↥Y) Set.univ (closure (Set.image (α := ↥X) (⇑f) Set.univ))

Tactic:
convert! subset_closure_inter_of_isPreirreducible_of_isOpen _ f.isOpenEmbedding.isOpen_range _

Premises used: subset_closure_inter_of_isPreirreducible_of_isOpen, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.isOpen_range
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
h : Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.range (ι := ↥X) ⇑f)
h₁ h₂ : Eq (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥X) ⇑f)
⊢ Eq (α := Set ↥Y) (Set.image (α := ↥X) (⇑f) Set.univ) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)

Tactic:
rw [Set.univ_inter, Set.image_univ]

Premises used: Set.image_univ, Set.univ_inter
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ IsPreirreducible.{u_1} (X := ↥Y) Set.univ

Tactic:
apply PreirreducibleSpace.isPreirreducible_univ (X := Y)

Premises used: PreirreducibleSpace.isPreirreducible_univ
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Set.Nonempty (α := ↥Y) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)

Tactic:
⟨_, trivial, Set.mem_range_self hX.2.some⟩

Premises used: Set.mem_range_self, trivial, Nonempty.some, IrreducibleSpace.toNonempty, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
hX : IrreducibleSpace.{u_1} ↥X
inst_1 : IrreducibleSpace.{u_1} ↥Y
⊢ Set.Nonempty (α := ↥Y) (Set.univ ∩ Set.range (ι := ↥X) ⇑f)

Tactic:
exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
x : ↥X
i : (↑(X.presheaf.stalk x) : Type u_1) →+* (↑X.functionField : Type u_1)
⊢ Algebra (↑(X.presheaf.stalk x) : Type u_1) (↑X.functionField : Type u_1)

Tactic:
apply RingHom.toAlgebra

Premises used: RingHom.toAlgebra
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
x : ↥X
⊢ (↑(X.presheaf.stalk x) : Type u_1) →+* (↑X.functionField : Type u_1)

Tactic:
exact (X.presheaf.stalkSpecializes ((genericPoint_spec X).specializes trivial)).hom

Premises used: CommRingCat.Hom.hom, trivial, AlgebraicGeometry.PresheafedSpace.carrier, IsGenericPoint.specializes, TopCat.Presheaf.stalkSpecializes, genericPoint_spec, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
U : X.Opens
x : ↥U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
h :
  Eq.{u_1 + 1} (α := (↑Γ(X, U) : Type u_1) →+* (↑X.functionField : Type u_1))
    (algebraMap (↑Γ(X, U) : Type u_1) (↑X.functionField : Type u_1))
    (@RingHom.comp _ (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1) (↑X.functionField : Type u_1))
      (algebraMap (↑Γ(X, U) : Type u_1) (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1)))
⊢ IsScalarTower.{u_1, u_1, u_1} (↑Γ(X, U) : Type u_1) (↑(X.presheaf.stalk (↑x : ↥X)) : Type u_1)
    (↑X.functionField : Type u_1)

Tactic:
apply IsScalarTower.of_algebraMap_eq'

Premises used: IsScalarTower.of_algebraMap_eq'
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
U : X.Opens
x : ↥U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
h :
  Eq (α := (↑(X.presheaf.obj (op U)) : Type u_1) →+* (↑X.functionField : Type u_1))
    (CommRingCat.Hom.hom (X.germToFunctionField U))
    (CommRingCat.Hom.hom (X.presheaf.germ U (↑x : ↥X) ⋯ ≫ X.presheaf.stalkSpecializes ⋯))
⊢ Eq (α := (↑Γ(X, U) : Type u_1) →+* (↑X.functionField : Type u_1)) (CommRingCat.Hom.hom (X.germToFunctionField U))
    (RingHom.comp (CommRingCat.Hom.hom (X.presheaf.stalkSpecializes ⋯))
      (CommRingCat.Hom.hom (X.presheaf.germ U (↑x : ↥X) ⋯)))

Tactic:
change _ = (X.presheaf.germ U x x.2 ≫ _).hom

Premises used: CommRingCat.Hom.hom, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, AlgebraicGeometry.Scheme.toLocallyRingedSpace, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IrreducibleSpace.{u_1} ↥X
U : X.Opens
x : ↥U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
h h₁ :
  Eq (α := (↑(X.presheaf.obj (op U)) : Type u_1) →+* (↑X.functionField : Type u_1))
    (CommRingCat.Hom.hom (X.germToFunctionField U)) (CommRingCat.Hom.hom (X.presheaf.germ U (genericPoint ↥X) ⋯))
⊢ Eq (α := (↑(X.presheaf.obj (op U)) : Type u_1) →+* (↑X.functionField : Type u_1))
    (CommRingCat.Hom.hom (X.germToFunctionField U))
    (CommRingCat.Hom.hom (X.presheaf.germ U (↑x : ↥X) ⋯ ≫ X.presheaf.stalkSpecializes ⋯))

Tactic:
rw [X.presheaf.germ_stalkSpecializes]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, TopCat.Presheaf.germ_stalkSpecializes, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
f : R.Hom (Spec R).functionField
⊢ (↑R : Type u) →+* (↑(Spec R).functionField : Type u)

Tactic:
apply CommRingCat.Hom.hom

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ R.Hom (Spec R).functionField

Tactic:
apply StructureSheaf.toStalk

Premises used: AlgebraicGeometry.StructureSheaf.toStalk
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
apply : IsGenericPoint.{u_1} (α := ↥(Spec R)) ⊥ Set.univ
⊢ Eq.{u_1 + 1} (α := ↥(Spec R)) (genericPoint ↥(Spec R)) ⊥

Tactic:
apply (genericPoint_spec (Spec R)).eq

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.PresheafedSpace.carrier, genericPoint_spec, IsGenericPoint.eq, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
rw : Eq (α := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus (↑(PrimeSpectrum.asIdeal ⊥) : Set (↑R : Type u_1))) Set.univ
⊢ Eq (α := Set ↥(Spec R)) (closure {⊥}) Set.univ

Tactic:
rw [← PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure, PrimeSpectrum.vanishingIdeal_singleton]

Premises used: PrimeSpectrum.vanishingIdeal_singleton, PrimeSpectrum.zeroLocus_vanishingIdeal_eq_closure
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
rw :
  Eq (α := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus (↑(PrimeSpectrum.asIdeal ⊥) : Set (↑R : Type u_1)))
    (PrimeSpectrum.zeroLocus {0})
⊢ Eq (α := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus (↑(PrimeSpectrum.asIdeal ⊥) : Set (↑R : Type u_1))) Set.univ

Tactic:
rw [← PrimeSpectrum.zeroLocus_singleton_zero]

Premises used: PrimeSpectrum.zeroLocus_singleton_zero
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
R : CommRingCat
inst : IsDomain.{u_1} (↑R : Type u_1)
⊢ Eq (α := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus (↑(PrimeSpectrum.asIdeal ⊥) : Set (↑R : Type u_1)))
    (PrimeSpectrum.zeroLocus {0})

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
⊢ IsLocalization.AtPrime.{u, u} (R := (↑R : Type u))
    (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
          (genericPoint ↥(Spec R))) :
      Type u)
    (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R)))

Tactic:
StructureSheaf.IsLocalization.to_stalk R (genericPoint (Spec R))

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, CommRingCat.carrier, AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, genericPoint, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
a :
  IsFractionRing.{u, u} (↑R : Type u) (↑(Spec R).functionField : Type u) ↔
    IsLocalization.AtPrime.{u, u} (R := (↑R : Type u))
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
            (genericPoint ↥(Spec R))) :
        Type u)
      (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R)))
⊢ IsFractionRing.{u, u} (↑R : Type u) (↑(Spec R).functionField : Type u)

Tactic:
convert! StructureSheaf.IsLocalization.to_stalk R (genericPoint (Spec R))

Premises used: AlgebraicGeometry.Spec, AlgebraicGeometry.StructureSheaf.IsLocalization.to_stalk, CommRingCat.carrier, AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, genericPoint, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
a :
  IsLocalization.{u, u} (R := (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (↑(Spec R).functionField : Type u) =
    IsLocalization.{u, u} (R := (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
            (genericPoint ↥(Spec R))) :
        Type u)
⊢ IsLocalization.{u, u} (R := (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (↑(Spec R).functionField : Type u) ↔
    IsLocalization.{u, u} (R := (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
            (genericPoint ↥(Spec R))) :
        Type u)

Tactic:
apply Eq.to_iff

Premises used: Eq.to_iff
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
a :
  Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u))
    (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
⊢ IsLocalization.{u, u} (R := (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (↑(Spec R).functionField : Type u) =
    IsLocalization.{u, u} (R := (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))
      (↑(Presheaf.stalk (X := PrimeSpectrum.Top (↑R : Type u)) (Sheaf.presheaf (Spec.structureSheaf (↑R : Type u)))
            (genericPoint ↥(Spec R))) :
        Type u)

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
a :
  Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))
⊢ Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u))
    (Ideal.primeCompl (PrimeSpectrum.asIdeal (genericPoint ↥(Spec R))))

Tactic:
rw [genericPoint_eq_bot_of_affine]

Premises used: AlgebraicGeometry.genericPoint_eq_bot_of_affine
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
a :
  ∀ (x : (↑R : Type u)),
    Membership.mem (γ := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) x ↔
      Membership.mem (γ := Submonoid (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥)) x
⊢ Eq.{u + 1} (α := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
x : (↑R : Type u)
⊢ Membership.mem (γ := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) x ↔
    Membership.mem (γ := Submonoid (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥)) x

Tactic:
mem_nonZeroDivisors_iff_ne_zero

Premises used: Set.Mem, setOf, Set.singleton, mem_nonZeroDivisors_iff_ne_zero, Not
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
R : CommRingCat
inst : IsDomain.{u} (↑R : Type u)
x : (↑R : Type u)
⊢ Membership.mem (γ := Submonoid (↑R : Type u)) (nonZeroDivisors (↑R : Type u)) x ↔
    Membership.mem (γ := Submonoid (↑R : Type u)) (Ideal.primeCompl (PrimeSpectrum.asIdeal ⊥)) x

Tactic:
exact mem_nonZeroDivisors_iff_ne_zero

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X_1 : Scheme
X : Scheme
inst : IsIntegral X
U : X.Opens
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ IsIntegral.{u_1} (↑U : Scheme)

Tactic:
isIntegral_of_isOpenImmersion U.ι

Premises used: AlgebraicGeometry.isIntegral_of_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X_1 : Scheme
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ (Set.univ ∩ (↑U : Set ↥X)).Nonempty

Tactic:
simpa using h
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ Eq (α := ↥(Spec (X.presheaf.obj (op U))))
    ((Iso.hom (↑U : Scheme).isoSpec ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))))
      (genericPoint ↥(↑U : Scheme)))
    (genericPoint ↥(Spec (X.presheaf.obj (op U))))

Tactic:
genericPoint_eq_of_isOpenImmersion
      (U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))

Premises used: Quiver.Hom.op, TopologicalSpace.Opens.isOpenEmbedding_obj_top, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Spec.map, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
h₁ :
  PrimeSpectrum (↑Γ(X, U) : Type u_1) = ↥(Spec (X.presheaf.obj (op U))) →
    Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯ = genericPoint ↥(↑U : Scheme)
⊢ Eq (α := PrimeSpectrum (↑Γ(X, U) : Type u_1))
    (hU.isoSpec.hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯) : ↥(Spec Γ(X, U)))
    (genericPoint ↥(Spec Γ(X, U)) : ↥(Spec Γ(X, U)))

Tactic:
convert!
    genericPoint_eq_of_isOpenImmersion
      (U.toScheme.isoSpec.hom ≫ Spec.map (X.presheaf.map (eqToHom U.isOpenEmbedding_obj_top).op))
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
e_1 : PrimeSpectrum (↑Γ(X, U) : Type u_1) = ↥(Spec (X.presheaf.obj (op U)))
h₁ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯) : ↥X) = (↑(genericPoint ↥(↑U : Scheme)) : ↥X)
⊢ Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯ = genericPoint ↥(↑U : Scheme)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
e_1 : PrimeSpectrum (↑Γ(X, U) : Type u_1) = ↥(Spec (X.presheaf.obj (op U)))
⊢ (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯) : ↥X) = (↑(genericPoint ↥(↑U : Scheme)) : ↥X)

Tactic:
(genericPoint_eq_of_isOpenImmersion U.ι).symm

Premises used: IsIrreducible.genericPoint, AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, genericPoint, AlgebraicGeometry.Scheme.Opens.ι, Classical.choose, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
h : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
e_1 : PrimeSpectrum (↑Γ(X, U) : Type u_1) = ↥(Spec (X.presheaf.obj (op U)))
⊢ (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯) : ↥X) = (↑(genericPoint ↥(↑U : Scheme)) : ↥X)

Tactic:
exact (genericPoint_eq_of_isOpenImmersion U.ι).symm

Premises used: AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion, AlgebraicGeometry.Scheme.Opens.ι, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 simpa : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
⊢ (Set.univ ∩ (↑U : Set ↥X)).Nonempty

Tactic:
simpa using ‹Nonempty U›

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, Nonempty, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.FunctionField
Goal:
X : Scheme
inst : IsIntegral X
U : X.Opens
hU : IsAffineOpen U
inst_1 : Nonempty.{u_1 + 1} ↥(↑U : Scheme)
h :
  nonZeroDivisors (↑Γ(X, U) : Type u_1) =
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (genericPoint ↥X) ⋯)).asIdeal.primeCompl
⊢ IsLocalization.{u_1, u_1} (R := (↑Γ(X, U) : Type u_1)) (nonZeroDivisors (↑Γ(X, U) : Type u_1))
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u_1)

Tactic:
convert!
    hU.isLocalization_stalk
      ⟨genericPoint X,
        (((genericPoint_spec X).mem_open_set_iff U.isOpen).mpr (by simpa using ‹Nonempty U›))⟩
    using 1

Premises used: Iff.mpr, AlgebraicGeometry.PresheafedSpace.carrier, genericPoint_spec, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, genericPoint, TopologicalSpace.Opens.isOpen, AlgebraicGeometry.IsAffineOpen.isLocalization_stalk, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, IsGenericPoint.mem_open_set_iff, AlgebraicGeometry.Scheme.toLocallyRingedSpace