awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.StructureSheaf (goal)
Goal:
R : Type u
inst : CommRing R
S : Type u
inst_1 : CommRing S
P : Type u
inst_2 : CommRing P
f : R →+* S
g : S →+* P
U : Opens (↑(PrimeSpectrum.Top R) : Type u)
V : Opens (↑(PrimeSpectrum.Top S) : Type u)
W : Opens (↑(PrimeSpectrum.Top P) : Type u)
hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U
hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
          CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u)))
          (structureSheaf R))
        (op U)) :
    Type u)
p : ↥(unop (op W))
rw :
  Eq (α := Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
    ((RingHom.comp (β := Localization.AtPrime (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal)
            (Localization.localRingHom (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
              (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal g ⋯)
            (Localization.localRingHom (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
              (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal f ⋯) :
          (a : Localization.AtPrime (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal) →
            Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal)
        ((↑s : (x : ↥(unop (op U))) → Localizations R (↑x : (↑(PrimeSpectrum.Top R) : Type u)))
          (Subtype.mk (p := fun (x : (↑(PrimeSpectrum.Top R) : Type u)) ↦ x ∈ unop (op U))
            (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))) ⋯)) :
      Localization.AtPrime (↑p : (↑(PrimeSpectrum.Top P) : Type u)).asIdeal)
    ((↑(((comap g V W hVW).comp (comap f U V hUV) :
                (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf P).obj.obj (op W)) : Type u))
              s) :
          (x : ↥(unop (op W))) → Localizations P (↑x : (↑(PrimeSpectrum.Top P) : Type u)))
        p :
      Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
⊢ Eq.{u + 1} (α := Localizations P (↑p : (↑(PrimeSpectrum.Top P) : Type u)))
    ((↑((comap (g.comp f) U W ⋯ :
              (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf P).obj.obj (op W)) : Type u))
            s) :
        (x : ↥(unop (op W))) → Localizations P (↑x : (↑(PrimeSpectrum.Top P) : Type u)))
      p)
    ((↑(((comap g V W hVW).comp (comap f U V hUV) :
              (a : (↑((structureSheaf R).obj.obj (op U)) : Type u)) → (↑((structureSheaf P).obj.obj (op W)) : Type u))
            s) :
        (x : ↥(unop (op W))) → Localizations P (↑x : (↑(PrimeSpectrum.Top P) : Type u)))
      p)
have hIJ : (PrimeSpectrum.comap (g.comp f) (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal =
  Ideal.comap f (PrimeSpectrum.comap g (↑p : (↑(PrimeSpectrum.Top P) : Type u))).asIdeal
Tactic: rw [comap_apply, Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} (Unique ⋯.LiftStruct)) ↔
    (∀ (x : ValuativeCommSq f), ⋯.HasLift) ∧ ∀ (x : ValuativeCommSq f), Subsingleton.{u + 1} ⋯.LiftStruct
have simp_rw : (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} (Unique sorry.LiftStruct)) ↔
  ∀ (x : ValuativeCommSq f), sorry.HasLift ∧ Subsingleton.{u + 1} sorry.LiftStruct
Tactic: simp_rw [← forall_and, unique_iff_subsingleton_and_nonempty, and_comm, CommSq.HasLift.iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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
⊢ (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} (Unique ⋯.LiftStruct)) ↔
    (∀ (x : ValuativeCommSq f), ⋯.HasLift) ∧ ∀ (x : ValuativeCommSq f), Subsingleton.{u + 1} ⋯.LiftStruct
have simp_rw₁ : (∀ (x : ValuativeCommSq f), Subsingleton.{u + 1} sorry.LiftStruct ∧ Nonempty.{u + 1} sorry.LiftStruct) ↔
  ∀ (x : ValuativeCommSq f), sorry.HasLift ∧ Subsingleton.{u + 1} sorry.LiftStruct
Tactic: simp_rw [← forall_and, unique_iff_subsingleton_and_nonempty, and_comm, CommSq.HasLift.iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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
⊢ (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} (Unique ⋯.LiftStruct)) ↔
    (∀ (x : ValuativeCommSq f), ⋯.HasLift) ∧ ∀ (x : ValuativeCommSq f), Subsingleton.{u + 1} ⋯.LiftStruct
have simp_rw₂ : (∀ (x : ValuativeCommSq f), Nonempty.{u + 1} sorry.LiftStruct ∧ Subsingleton.{u + 1} sorry.LiftStruct) ↔
  ∀ (x : ValuativeCommSq f), sorry.HasLift ∧ Subsingleton.{u + 1} sorry.LiftStruct
Tactic: simp_rw [← forall_and, unique_iff_subsingleton_and_nonempty, and_comm, CommSq.HasLift.iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
⊢ ValuativeCriterion = Existence ⊓ Uniqueness
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), ValuativeCriterion f ↔ (Existence ⊓ Uniqueness) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y
have 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
Tactic: obtain ⟨A, hA, hA_local⟩ := exists_factor_valuationRing stalk_y_to_residue_x'.hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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
have 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
Tactic: rw [Scheme.fromSpecResidueField, Category.assoc, ← Scheme.SpecMap_stalkMap_fromSpecStalk,
      ← Scheme.SpecMap_stalkSpecializes_fromSpecStalk h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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 (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
have 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
Tactic: simp_rw [← Spec.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
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)
⊢ ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y
have 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
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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
have refine_1 : flip (β := ↥X) (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) (l (closedPoint ↥A) : ↥X) x'
Tactic: refine ⟨l (closedPoint A), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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'
⊢ ∃ (a' : ↥X), flip (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) a' x' ∧ f a' = y
have refine_2 : f (l (closedPoint ↥A) : ↥X) = y
Tactic: refine ⟨l (closedPoint A), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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) (fun (x1 x2 : ↥X) ↦ x1 ⤳ x2) (l (closedPoint ↥A) : ↥X) x'
have 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)
Tactic: simp_rw [← Scheme.fromSpecResidueField_apply x' (closedPoint (X.residueField x')), ← hl₁]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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
⊢ f (l (closedPoint ↥A) : ↥X) = y
have refine_2 : (Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y) (closedPoint ↥A) = y
Tactic: rw [← Scheme.Hom.comp_apply, hl₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
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
⊢ (Y.fromSpecStalk y) ((Spec.map stalk_y_to_A) (closedPoint ↥A) : ↥(Spec (Y.presheaf.stalk y))) = y
have this : Eq (α := ↥(Spec (Y.presheaf.stalk y))) ((Spec.map stalk_y_to_A) (closedPoint ↥A) : ↥(Spec (Y.presheaf.stalk y)))
  (closedPoint (↑(Y.presheaf.stalk y) : Type u) : PrimeSpectrum (↑(Y.presheaf.stalk y) : Type u))
Tactic: have : Spec.map stalk_y_to_A (closedPoint A) = closedPoint (Y.presheaf.stalk y) :=
      comap_closedPoint (S := A) (stalk_y_to_residue_x'.hom.codRestrict A.toSubring hA)