awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
⊢ φ ≫ CommRingCat.ofHom (algebraMap R K) = β

Tactic:
have hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β :=
    hαβ ▸ CommRingCat.hom_ext (RingHom.ext fun x ↦ congr_arg Subtype.val
      ((RingEquiv.ofBijective _ hbij).apply_symm_apply (β.hom.rangeRestrict x)))
-- 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
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β
⊢ ⋯.HasLift

Tactic:
⟨⟨⟨Spec.map ((pullback.snd i₂ f).stalkMap x ≫ φ) ≫ X.fromSpecStalk _, ?_, ?_⟩⟩⟩

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Spec.map, Nonempty.intro, CategoryTheory.CommSq.LiftStruct.mk, CategoryTheory.CommSq.HasLift.mk, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.fromSpecStalk, AlgebraicGeometry.Scheme.Hom.stalkMap
-- 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
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β
refine_1 : lft ≫ pullback.snd i₂ f = i₁
⊢ CategoryStruct.comp (Y := Spec ((pullback i₂ f).presheaf.stalk (lft (closedPoint K))))
      (Spec.map (Scheme.stalkClosedPointTo lft))
      ((pullback i₂ f).fromSpecStalk (lft (closedPoint K)) ≫ pullback.snd i₂ f) =
    i₁

Tactic:
rw [Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc]

Premises used: AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk_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
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β
⊢ lft ≫ pullback.snd i₂ f = i₁

Tactic:
simp [lft]
-- 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
hαβ : α ≫ β = CommRingCat.ofHom (algebraMap R K)
hbij :
  Function.Bijective (α := R) (β := ↥(CommRingCat.Hom.hom β).range)
    (⇑(RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) :
      (a : R) → ↥(CommRingCat.Hom.hom β).range)
φ : (pullback i₂ f).presheaf.stalk x ⟶ CommRingCat.of R :=
  CommRingCat.ofHom
    (RingHom.comp
      (RingEquiv.toRingHom
        (RingEquiv.symm
          (RingEquiv.ofBijective (RingHom.comp (CommRingCat.Hom.hom β).rangeRestrict (CommRingCat.Hom.hom α)) hbij)))
      (CommRingCat.Hom.hom β).rangeRestrict)
hαφ : α ≫ φ = 𝟙 (CommRingCat.of R)
hαφ' : Scheme.Hom.stalkMap (pullback.fst i₂ f) x ≫ φ = e.inv
hφβ : φ ≫ CommRingCat.ofHom (algebraMap R K) = β
refine_2 : Spec.map e.inv ≫ (Spec (CommRingCat.of R)).fromSpecStalk ((pullback.fst i₂ f) x) ≫ i₂ = i₂
⊢ Spec.map φ ≫ (pullback i₂ f).fromSpecStalk x ≫ pullback.fst i₂ f ≫ i₂ = i₂

Tactic:
rw [← Scheme.SpecMap_stalkMap_fromSpecStalk_assoc, ← Spec.map_comp_assoc, hαφ']

Premises used: AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Scheme.SpecMap_stalkMap_fromSpecStalk_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
of_isPullback :
  ∀ {X Y Y' S : Scheme.{u_1}} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X} (sq : IsPullback f' g' g f)
    (hg : Existence g), Existence g'
⊢ Existence.IsStableUnderBaseChange

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
⊢ (commSq.i₁ ≫ X'_to_X) ≫ f = Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ ≫ Y'_to_Y

Tactic:
simp only [Category.assoc, hP.w, reassoc_of% commSq.commSq.w]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.ValuativeCommSq.commSq, CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
of_isPullback :
  ∀ (l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X)
    (hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁) (hl₂ : l₀ ≫ f = commSq'.i₂),
    ⋯.HasLift
⊢ ⋯.HasLift

Tactic:
obtain ⟨l₀, hl₁, hl₂⟩ := (hf commSq').exists_lift

Premises used: CategoryTheory.CommSq.HasLift.exists_lift
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ l₀ ≫ f = commSq.i₂ ≫ Y'_to_Y

Tactic:
simp_all only [commSq']
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
of_isPullback : Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯ = commSq.i₁
⊢ ⋯.HasLift

Tactic:
refine ⟨⟨⟨hP.lift l₀ commSq.i₂ (by simp_all only [commSq']), ?_, hP.lift_snd _ _ _⟩⟩⟩
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
of_isPullback :
  (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ X'_to_X = commSq.i₁ ≫ X'_to_X
of_isPullback₁ :
  (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ f' = commSq.i₁ ≫ f'
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯ = commSq.i₁

Tactic:
apply hP.hom_ext

Premises used: CategoryTheory.IsPullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
⊢ (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ X'_to_X = commSq.i₁ ≫ X'_to_X

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
of_isPullback :
  Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯ ≫ f' = commSq.i₁ ≫ f'
⊢ (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯) ≫ f' = commSq.i₁ ≫ f'

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
of_isPullback : Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ = commSq.i₁ ≫ f'
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯ ≫ f' = commSq.i₁ ≫ f'

Tactic:
rw [hP.lift_snd]

Premises used: CategoryTheory.IsPullback.lift_snd
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y' X X' Y : Scheme
Y'_to_Y : Y' ⟶ Y
f : X ⟶ Y
X'_to_X : X' ⟶ X
f' : X' ⟶ Y'
hP : IsPullback X'_to_X f' f Y'_to_Y
hf : Existence f
commSq : ValuativeCommSq f'
commSq' : ValuativeCommSq f :=
  { R := commSq.R, commRing := commSq.commRing, domain := ⋯, valuationRing := ⋯, K := commSq.K, field := commSq.field,
    algebra := commSq.algebra, isFractionRing := ⋯, i₁ := commSq.i₁ ≫ X'_to_X, i₂ := commSq.i₂ ≫ Y'_to_Y, commSq := ⋯ }
l₀ : Spec (CommRingCat.of commSq'.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap commSq'.R commSq'.K)) ≫ l₀ = commSq'.i₁
hl₂ : l₀ ≫ f = commSq'.i₂
of_isPullback of_isPullback₁ :
  Eq (α := Spec (CommRingCat.of commSq.K) ⟶ Y')
    (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂)
    (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂)
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ = commSq.i₁ ≫ f'

Tactic:
rw [commSq.commSq.w]

Premises used: AlgebraicGeometry.ValuativeCommSq.commSq, CategoryTheory.CommSq.w
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), Existence f ↔ (topologically @SpecializingMap).universally f
⊢ Existence = (topologically @SpecializingMap).universally

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
h : Existence f → (topologically @SpecializingMap).universally f
h₁ : (topologically @SpecializingMap).universally f → Existence f
⊢ Existence f ↔ (topologically @SpecializingMap).universally f

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
h_1 : Existence f
h : Existence ≤ topologically @SpecializingMap
h₁ : Existence.universally f
h₂ : MorphismProperty Scheme
⊢ (topologically @SpecializingMap).universally f

Tactic:
apply MorphismProperty.universally_mono

Premises used: CategoryTheory.MorphismProperty.universally_mono
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
h : Existence f
⊢ Existence ≤ topologically @SpecializingMap

Tactic:
apply specializingMap

Premises used: AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
h_1 h h₁ h₂ h₃ : Existence f
⊢ Existence.universally f

Tactic:
rwa [MorphismProperty.IsStableUnderBaseChange.universally_eq]

Premises used: CategoryTheory.MorphismProperty.IsStableUnderBaseChange.universally_eq
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (topologically @SpecializingMap).universally f → Existence f

Tactic:
apply of_specializingMap

Premises used: AlgebraicGeometry.ValuativeCriterion.Existence.of_specializingMap