awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 : (Spec.map stalk_y_to_A ≫ Y.fromSpecStalk y) (closedPoint ↥A) = y
⊢ f (l (closedPoint ↥A) : ↥X) = y

Tactic:
rw [← Scheme.Hom.comp_apply, hl₂]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_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
⊢ 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)
-- 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
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
refine_2₁ refine_2₂ : y = y
⊢ (Y.fromSpecStalk y) ((Spec.map stalk_y_to_A) (closedPoint ↥A) : ↥(Spec (Y.presheaf.stalk y))) = y

Tactic:
rw [this, Y.fromSpecStalk_closedPoint]

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
e : R ≅ S
⊢ IsLocalHom (R := (↑R : Type u_1)) (S := (↑S : Type u_1)) (CommRingCat.Hom.hom e.hom)

Tactic:
isLocalHom_of_isIso _

Premises used: isLocalHom_of_isIso
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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₂
⊢ IsDomain.{u} (↑(CommRingCat.of R) : Type u)

Tactic:
haveI : IsDomain (CommRingCat.of R) := ‹_›
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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)
⊢ ValuationRing.{u} (↑(CommRingCat.of R) : Type u)

Tactic:
haveI : ValuationRing (CommRingCat.of R) := ‹_›
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
⊢ 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)
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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₁ ⋯
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)),
    ⋯.HasLift
⊢ ⋯.HasLift

Tactic:
obtain ⟨x, h₁, h₂⟩ := @H (lft (closedPoint _)) _ (specializes_closedPoint (R := R) _)

Premises used: IsLocalRing.specializes_closedPoint
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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)
⊢ 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))
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
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)) ⋯ ≫
          Scheme.stalkClosedPointTo lft) =
    CommRingCat.ofHom (algebraMap R K)
⊢ 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)

Tactic:
simp only [TopCat.Presheaf.germ_stalkSpecializes_assoc, Scheme.Hom.germ_stalkMap_assoc]

Premises used: AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, TopCat.Presheaf.germ_stalkSpecializes_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
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 ⋯)) ≪≫
              Scheme.ΓSpecIso (CommRingCat.of K))) =
    CommRingCat.ofHom (algebraMap R K)
⊢ 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)

Tactic:
rw [Scheme.germ_stalkClosedPointTo lft ⊤ trivial]

Premises used: AlgebraicGeometry.Scheme.germ_stalkClosedPointTo, trivial, Top.top
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
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))
⊢ 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)

Tactic:
erw [← Scheme.Hom.comp_app_assoc lft (pullback.fst i₂ f)]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_app_assoc, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
rw :
  Eq (α := CommRingCat.of R ⟶ CommRingCat.of K)
    (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of R)) ≫
      CategoryStruct.comp (Y := Γ(Spec (CommRingCat.of K), Spec.map (CommRingCat.ofHom (algebraMap R K)) ⁻¹ᵁ ⊤))
        (Scheme.Hom.app (Spec.map (CommRingCat.ofHom (algebraMap R K))) ⊤)
        (Iso.hom (Scheme.ΓSpecIso (CommRingCat.of K))))
    (CommRingCat.ofHom (algebraMap R K))
⊢ 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:
rw [pullback.lift_fst]

Premises used: CategoryTheory.Limits.pullback.lift_fst