awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.StructureSheaf
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
f : R →+* S
x : R
⊢ Eq (α :=
    R →+*
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top S) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
              (structureSheaf S))
            (op (basicOpen ((f : (a : R) → S) x)))) :
        Type u))
    (RingHom.comp (β :=
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op (basicOpen x))) :
        Type u))
      (comap f (basicOpen x) (basicOpen ((f : (a : R) → S) x)) ⋯)
      (algebraMap R
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheaf R))
              (op (basicOpen x))) :
          Type u)))
    (@RingHom.comp _
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
              (structureSheaf R))
            (op (basicOpen x))) :
        Type u)
      _ _ Semiring.toNonAssocSemiring _
      (IsLocalization.map (M := Submonoid.powers x) (T := Submonoid.powers ((f : (a : R) → S) x))
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top S) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top S) : Type u)))
                (structureSheaf S))
              (op (basicOpen ((f : (a : R) → S) x)))) :
          Type u)
        f ⋯)
      (algebraMap R
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
                (structureSheaf R))
              (op (basicOpen x))) :
          Type u)))

Tactic:
simpa [CommRingCat.hom_ext_iff] using toOpen_comp_comap f _

Premises used: AlgebraicGeometry.StructureSheaf.toOpen_comp_comap, CommRingCat.hom_ext_iff
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
simp_rw :
  (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} (Unique ⋯.LiftStruct)) ↔
    ∀ (x : ValuativeCommSq f), ⋯.HasLift ∧ Subsingleton.{u + 1} ⋯.LiftStruct
simp_rw₁ :
  (∀ (x : ValuativeCommSq f), Subsingleton.{u + 1} ⋯.LiftStruct ∧ Nonempty.{u + 1} ⋯.LiftStruct) ↔
    ∀ (x : ValuativeCommSq f), ⋯.HasLift ∧ Subsingleton.{u + 1} ⋯.LiftStruct
simp_rw₂ :
  (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} ⋯.LiftStruct ∧ Subsingleton.{u + 1} ⋯.LiftStruct) ↔
    ∀ (x : ValuativeCommSq f), ⋯.HasLift ∧ Subsingleton.{u + 1} ⋯.LiftStruct
⊢ (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} (Unique ⋯.LiftStruct)) ↔
    (∀ (x : ValuativeCommSq f), ⋯.HasLift) ∧ ∀ (x : ValuativeCommSq f), Subsingleton.{u + 1} ⋯.LiftStruct

Tactic:
simp_rw [← forall_and, unique_iff_subsingleton_and_nonempty, and_comm, CommSq.HasLift.iff]

Premises used: and_comm, unique_iff_subsingleton_and_nonempty, forall_and, CategoryTheory.CommSq.HasLift.iff
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), ValuativeCriterion f ↔ (Existence ⊓ Uniqueness) f
⊢ ValuativeCriterion = Existence ⊓ Uniqueness

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion f ↔ (Existence ⊓ Uniqueness) f

Tactic:
iff

Premises used: AlgebraicGeometry.ValuativeCriterion.iff
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion f ↔ (Existence ⊓ Uniqueness) f

Tactic:
exact iff

Premises used: AlgebraicGeometry.ValuativeCriterion.iff
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
h : ValuativeCriterion f
⊢ Existence f

Tactic:
(iff.mp h).1

Premises used: AlgebraicGeometry.ValuativeCriterion.iff, And.left, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
h : ValuativeCriterion f
⊢ Uniqueness f

Tactic:
(iff.mp h).2

Premises used: AlgebraicGeometry.ValuativeCriterion.iff, And.right, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
obtain :
  ∀ (A : ValuationSubring (↑(X.residueField x') : Type u))
    (hA :
      ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
        Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
          ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
                (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
              x :
            (↑(X.residueField x') : Type u)))
    (hA_local :
      IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
        (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
        ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)),
    ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y
⊢ ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y

Tactic:
obtain ⟨A, hA, hA_local⟩ := exists_factor_valuationRing stalk_y_to_residue_x'.hom

Premises used: CommRingCat.Hom.hom, IsLocalRing.exists_factor_valuationRing
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
rw :
  Spec.map (X.residue x') ≫
      Spec.map (Scheme.Hom.stalkMap f x') ≫ Spec.map (Y.presheaf.stalkSpecializes h) ≫ Y.fromSpecStalk y =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y

Tactic:
rw [Scheme.fromSpecResidueField, Category.assoc, ← Scheme.SpecMap_stalkMap_fromSpecStalk,
      ← Scheme.SpecMap_stalkSpecializes_fromSpecStalk h]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk, AlgebraicGeometry.Scheme.fromSpecResidueField, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
simp_rw :
  Spec.map ((Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x') ≫ X.residue x') ≫ Y.fromSpecStalk y =
    Spec.map (stalk_y_to_A ≫ CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ Y.fromSpecStalk y
⊢ Spec.map (X.residue x') ≫
      Spec.map (Scheme.Hom.stalkMap f x') ≫ Spec.map (Y.presheaf.stalkSpecializes h) ≫ Y.fromSpecStalk y =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y

Tactic:
simp_rw [← Spec.map_comp_assoc]

Premises used: AlgebraicGeometry.Spec.map_comp_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
⊢ Spec.map ((Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x') ≫ X.residue x') ≫ Y.fromSpecStalk y =
    Spec.map (stalk_y_to_A ≫ CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ Y.fromSpecStalk y

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
⊢ X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y

Tactic:
have w : X.fromSpecResidueField x' ≫ f =
      Spec.map (CommRingCat.ofHom (algebraMap A (X.residueField x'))) ≫
        Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y := by
    rw [Scheme.fromSpecResidueField, Category.assoc, ← Scheme.SpecMap_stalkMap_fromSpecStalk,
      ← Scheme.SpecMap_stalkSpecializes_fromSpecStalk h]
    simp_rw [← Spec.map_comp_assoc]
    rfl
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
            K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
            algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
            i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y

Tactic:
⟨l (closedPoint A), ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Membership.mem, Subtype, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, IsLocalRing.closedPoint, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
            K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
            algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
            i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
refine_1 : flip (β := ↥X) (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) (l (closedPoint ↥A) : ↥X) x'
refine_2 : f (l (closedPoint ↥A) : ↥X) = y
⊢ ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y

Tactic:
refine ⟨l (closedPoint A), ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
            K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
            algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
            i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
refine_1 :
  flip (α := ↥X) (β := ↥X) (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) (l (closedPoint ↥A) : ↥X)
    ((Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l)
        (closedPoint (↑(X.residueField x') : Type u)) :
      ↥X)
⊢ flip (β := ↥X) (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) (l (closedPoint ↥A) : ↥X) x'

Tactic:
simp_rw [← Scheme.fromSpecResidueField_apply x' (closedPoint (X.residueField x')), ← hl₁]

Premises used: CommRingCat.carrier, AlgebraicGeometry.Scheme.residueField, IsLocalRing.closedPoint, AlgebraicGeometry.Scheme.fromSpecResidueField_apply
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
            K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
            algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
            i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ flip (α := ↥X) (β := ↥X) (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) (l (closedPoint ↥A) : ↥X)
    ((Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l)
        (closedPoint (↑(X.residueField x') : Type u)) :
      ↥X)

Tactic:
(specializes_closedPoint _).map l.continuous

Premises used: Specializes, Set.Mem, IsLocalRing.specializes_closedPoint, AlgebraicGeometry.Scheme.Hom.continuous, Specializes.map
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↥X
y : ↥Y
h : flip (α := ↥Y) (fun (x1 x2 : ↥Y) ↦ x1 ⤳ x2) y (f x' : ↥Y)
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring (↑(X.residueField x') : Type u)
hA :
  ∀ (x : (↑(Y.presheaf.stalk y) : Type u)),
    Membership.mem (α := (↑(X.residueField x') : Type u)) A.toSubring
      ((CommRingCat.Hom.hom stalk_y_to_residue_x' :
            (a : (↑(Y.presheaf.stalk y) : Type u)) → (↑(X.residueField x') : Type u))
          x :
        (↑(X.residueField x') : Type u))
hA_local :
  IsLocalHom (R := (↑(Y.presheaf.stalk y) : Type u)) (S := ↥A.toSubring) (F :=
    (↑(Y.presheaf.stalk y) : Type u) →+* ↥A.toSubring)
    ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
w :
  X.fromSpecResidueField x' ≫ f =
    Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫
      Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
l :
  Spec
      (CommRingCat.of
        { R := ↥A, commRing := A.instCommRingSubtypeMem, domain := ⋯, valuationRing := ⋯,
            K := (↑(X.residueField x') : Type u), field := X.instFieldCarrierResidueField x',
            algebra := A.instAlgebraSubtypeMem, isFractionRing := ⋯, i₁ := X.fromSpecResidueField x',
            i₂ := Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y, commSq := ⋯ : ValuativeCommSq f }.R) ⟶
    X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l = X.fromSpecResidueField x'
hl₂ : l ≫ f = Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y
⊢ flip (α := ↥X) (β := ↥X) (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) (l (closedPoint ↥A) : ↥X)
    ((Spec.map (CommRingCat.ofHom (algebraMap ↥A (↑(X.residueField x') : Type u))) ≫ l)
        (closedPoint (↑(X.residueField x') : Type u)) :
      ↥X)

Tactic:
exact (specializes_closedPoint _).map l.continuous

Premises used: IsLocalRing.specializes_closedPoint, AlgebraicGeometry.Scheme.Hom.continuous, Specializes.map