awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ (Y.fromSpecStalk y) ((Spec.map stalk_y_to_A) (closedPoint ↥A) : ↥(Spec (Y.presheaf.stalk y))) = y
have refine_2 : (Y.fromSpecStalk y) (closedPoint (↑(Y.presheaf.stalk y) : Type u)) = y
Tactic: rw [this, Y.fromSpecStalk_closedPoint]
-- 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
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))
refine_2 : (Y.fromSpecStalk y) (closedPoint (↑(Y.presheaf.stalk y) : Type u)) = y
⊢ (Y.fromSpecStalk y) ((Spec.map stalk_y_to_A) (closedPoint ↥A) : ↥(Spec (Y.presheaf.stalk y))) = y
have refine_2₁ : y = y
Tactic: rw [this, Y.fromSpecStalk_closedPoint]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H : (topologically @SpecializingMap).universally f
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
⊢ ⋯.HasLift
have this : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
Tactic: haveI : IsDomain (CommRingCat.of R) := ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H : (topologically @SpecializingMap).universally f
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
⊢ ⋯.HasLift
have this₁ : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
Tactic: haveI : ValuationRing (CommRingCat.of R) := ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
H : (topologically @SpecializingMap).universally f
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this : Field (↑(CommRingCat.of K) : Type u) := field
⊢ ⋯.HasLift
have H₁ : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
Tactic: replace H := H (pullback.snd i₂ f) i₂ (pullback.fst i₂ f) (.of_hasPullback i₂ f)
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
⊢ ⋯.HasLift
have obtain : ∀ (x : ↥(pullback i₂ f))
  (h₁ :
    flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
      (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f)))
  (h₂ :
    Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
      (closedPoint R : PrimeSpectrum R)),
  sorry.HasLift
Tactic: obtain ⟨x, h₁, h₂⟩ := @H (lft (closedPoint _)) _ (specializes_closedPoint (R := R) _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
⊢ ⋯.HasLift
have this₁ : IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
  (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
Tactic: have : IsLocalHom e.hom.hom := isLocalHom_of_isIso e.hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
⊢ ⋯.HasLift
have this₁ : IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
  (CommRingCat.Hom.hom α)
Tactic: have : IsLocalHom α.hom := inferInstanceAs
    (IsLocalHom (((pullback.fst i₂ f).stalkMap x).hom.comp e.hom.hom))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ α ≫ β = CommRingCat.ofHom (algebraMap R K)
have simp : Eq (α := CommRingCat.of R ⟶ CommRingCat.of K)
  (CategoryStruct.comp (Y :=
    CommRingCat.of
      (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
        (ObjectProperty.FullSubcategory.obj (P :=
          Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u))) (structureSheafInType R R))
        (Opposite.op ⊤)))
    (CommRingCat.ofHom
      (algebraMap R
        (Functor.obj (C := (TopologicalSpace.Opens (↑(PrimeSpectrum.Top R) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top R) : Type u))) (structureSheafInType R R))
          (Opposite.op ⊤))))
    (TopCat.Presheaf.germ (structurePresheafInCommRingCat R) ⊤ (closedPoint R) trivial ≫
      (Spec (CommRingCat.of R)).presheaf.stalkSpecializes sorry ≫
        Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫
          (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft))
  (CommRingCat.ofHom (algebraMap R K))
Tactic: simp only [CommRingCat.coe_of, Iso.trans_hom, Iso.symm_hom, TopCat.Presheaf.stalkCongr_hom,
      Category.assoc, α, e, β, stalkClosedPointIso_inv, StructureSheaf.toStalk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
      (Spec (CommRingCat.of R)).presheaf.germ ⊤ (closedPoint R) trivial ≫
        (Spec (CommRingCat.of R)).presheaf.stalkSpecializes ⋯ ≫
          Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫
            (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft =
    CommRingCat.ofHom (algebraMap R K)
have simp : Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
    CategoryStruct.comp (Y := Γ(pullback i₂ f, pullback.fst i₂ f ⁻¹ᵁ ⊤)) (Scheme.Hom.app (pullback.fst i₂ f) ⊤)
      ((pullback i₂ f).presheaf.germ (pullback.fst i₂ f ⁻¹ᵁ ⊤) (lft (closedPoint K)) sorry ≫
        Scheme.stalkClosedPointTo lft) =
  CommRingCat.ofHom (algebraMap R K)
Tactic: simp only [TopCat.Presheaf.germ_stalkSpecializes_assoc, Scheme.Hom.germ_stalkMap_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
      CategoryStruct.comp (Y := Γ(pullback i₂ f, ⊤))
        (Scheme.Hom.app (pullback.fst i₂ f) ⊤ :
          Γ(Spec (CommRingCat.of R), ⊤) ⟶ Γ(pullback i₂ f, pullback.fst i₂ f ⁻¹ᵁ ⊤))
        ((pullback i₂ f).presheaf.germ ⊤ (lft (closedPoint K)) ⋯ ≫ Scheme.stalkClosedPointTo lft) =
    CommRingCat.ofHom (algebraMap R K)
have rw : Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
    CategoryStruct.comp (Y := Γ(pullback i₂ f, ⊤))
      (Scheme.Hom.app (pullback.fst i₂ f) ⊤ : Γ(Spec (CommRingCat.of R), ⊤) ⟶ Γ(pullback i₂ f, pullback.fst i₂ f ⁻¹ᵁ ⊤))
      (Scheme.Hom.app lft ⊤ ≫
        Iso.hom
          (Functor.mapIso (Spec (CommRingCat.of K)).presheaf (Iso.op (eqToIso sorry)) ≪≫
            Scheme.ΓSpecIso (CommRingCat.of K))) =
  CommRingCat.ofHom (algebraMap R K)
Tactic: rw [Scheme.germ_stalkClosedPointTo lft ⊤ trivial]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u
commRing : CommRing R
domain : IsDomain R
valuationRing : ValuationRing R
K : Type u
field : Field K
algebra : Algebra R K
isFractionRing : IsFractionRing R K
i₁ : Spec (CommRingCat.of K) ⟶ X
i₂ : Spec (CommRingCat.of R) ⟶ Y
w : i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap R K)) ≫ i₂
this_1 : IsDomain.{u} (↑(CommRingCat.of R) : Type u)
this_2 : ValuationRing.{u} (↑(CommRingCat.of R) : Type u)
this_3 : Field (↑(CommRingCat.of K) : Type u) := field
H : topologically @SpecializingMap (X := pullback i₂ f) (pullback.fst i₂ f)
lft : Spec (CommRingCat.of K) ⟶ pullback i₂ f := pullback.lift (Spec.map (CommRingCat.ofHom (algebraMap R K))) i₁ ⋯
x : ↥(pullback i₂ f)
h₁ :
  flip (α := ↥(pullback i₂ f)) (fun (x1 x2 : ↥(pullback i₂ f)) ↦ x1 ⤳ x2) x
    (lft (closedPoint (↑(CommRingCat.of K) : Type u)) : ↥(pullback i₂ f))
h₂ :
  Eq (α := ↥(Spec (CommRingCat.of R))) ((pullback.fst i₂ f) x : ↥(Spec (CommRingCat.of R)))
    (closedPoint R : PrimeSpectrum R)
e : CommRingCat.of R ≅ (Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x) :=
  Iso.symm (stalkClosedPointIso (CommRingCat.of R)) ≪≫ (Spec (CommRingCat.of R)).presheaf.stalkCongr ⋯
α : CommRingCat.of R ⟶ (pullback i₂ f).presheaf.stalk x := e.hom ≫ Scheme.Hom.stalkMap (pullback.fst i₂ f) x
this_4 :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S :=
    (↑((Spec (CommRingCat.of R)).presheaf.stalk ((pullback.fst i₂ f) x)) : Type u)) (CommRingCat.Hom.hom e.hom)
this :
  IsLocalHom (R := (↑(CommRingCat.of R) : Type u)) (S := (↑((pullback i₂ f).presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom α)
β : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of K :=
  (pullback i₂ f).presheaf.stalkSpecializes h₁ ≫ Scheme.stalkClosedPointTo lft
⊢ Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
      CategoryStruct.comp (Y := Γ(pullback i₂ f, ⊤))
        (Scheme.Hom.app (pullback.fst i₂ f) ⊤ :
          Γ(Spec (CommRingCat.of R), ⊤) ⟶ Γ(pullback i₂ f, pullback.fst i₂ f ⁻¹ᵁ ⊤))
        (Scheme.Hom.app lft ⊤ ≫
          Iso.hom
            (Functor.mapIso (Spec (CommRingCat.of K)).presheaf (Iso.op (eqToIso ⋯)) ≪≫
              Scheme.ΓSpecIso (CommRingCat.of K))) =
    CommRingCat.ofHom (algebraMap R K)
have erw : Eq (α := CommRingCat.of R ⟶ CommRingCat.of K)
  (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
    Scheme.Hom.app (lft ≫ pullback.fst i₂ f) ⊤ ≫ Iso.hom (Scheme.ΓSpecIso (CommRingCat.of K)))
  (CommRingCat.ofHom (algebraMap R K))
Tactic: erw [← Scheme.Hom.comp_app_assoc lft (pullback.fst i₂ f)]