awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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 := ⋯ }
⊢ ⋯.HasLift
have 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₂),
  sorry.HasLift
Tactic: obtain ⟨l₀, hl₁, hl₂⟩ := (hf commSq').exists_lift
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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₂
⊢ ⋯.HasLift
have of_isPullback : Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ sorry = commSq.i₁
Tactic: refine ⟨⟨⟨hP.lift l₀ commSq.i₂ (by simp_all only [commSq']), ?_, hP.lift_snd _ _ _⟩⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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₂ ⋯ = commSq.i₁
have of_isPullback : (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ sorry) ≫ X'_to_X = commSq.i₁ ≫ X'_to_X
Tactic: apply hP.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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
⊢ Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ ⋯ = commSq.i₁
have of_isPullback₁ : (Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ sorry) ≫ f' = commSq.i₁ ≫ f'
Tactic: apply hP.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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₂ ⋯) ≫ f' = commSq.i₁ ≫ f'
have of_isPullback : Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ hP.lift l₀ commSq.i₂ sorry ≫ f' = commSq.i₁ ≫ f'
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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₂ ⋯ ≫ f' = commSq.i₁ ≫ f'
have of_isPullback : Spec.map (CommRingCat.ofHom (algebraMap commSq.R commSq.K)) ≫ commSq.i₂ = commSq.i₁ ≫ f'
Tactic: rw [hP.lift_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
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)) ≫ commSq.i₂ = commSq.i₁ ≫ f'
have 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₂)
Tactic: rw [commSq.commSq.w]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
⊢ Existence = (topologically @SpecializingMap).universally
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y), Existence f ↔ (topologically @SpecializingMap).universally f
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Existence f ↔ (topologically @SpecializingMap).universally f
have h : Existence f → (topologically @SpecializingMap).universally f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h : Existence f → (topologically @SpecializingMap).universally f
⊢ Existence f ↔ (topologically @SpecializingMap).universally f
have h₁ : (topologically @SpecializingMap).universally f → Existence f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h : Existence f
⊢ (topologically @SpecializingMap).universally f
have h : Existence ≤ topologically @SpecializingMap
Tactic: apply MorphismProperty.universally_mono
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h_1 : Existence f
h : Existence ≤ topologically @SpecializingMap
⊢ (topologically @SpecializingMap).universally f
have h₁ : Existence.universally f
Tactic: apply MorphismProperty.universally_mono
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h_1 : Existence f
h : Existence ≤ topologically @SpecializingMap
h₁ : Existence.universally f
⊢ (topologically @SpecializingMap).universally f
have h₂ : MorphismProperty Scheme
Tactic: apply MorphismProperty.universally_mono
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
⊢ @UniversallyClosed = ValuativeCriterion.Existence ⊓ @QuasiCompact
have rw : (topologically @SpecializingMap).universally ⊓ @QuasiCompact = ValuativeCriterion.Existence ⊓ @QuasiCompact
Tactic: rw [universallyClosed_eq_universallySpecializing, ValuativeCriterion.Existence.eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
rw : (topologically @SpecializingMap).universally ⊓ @QuasiCompact = ValuativeCriterion.Existence ⊓ @QuasiCompact
⊢ @UniversallyClosed = ValuativeCriterion.Existence ⊓ @QuasiCompact
have rw₁ : (topologically @SpecializingMap).universally ⊓ @QuasiCompact =
  (topologically @SpecializingMap).universally ⊓ @QuasiCompact
Tactic: rw [universallyClosed_eq_universallySpecializing, ValuativeCriterion.Existence.eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ UniversallyClosed f
have rw : (ValuativeCriterion.Existence ⊓ @QuasiCompact) f
Tactic: rw [eq_valuativeCriterion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have this : UniversallyClosed (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: have := UniversallyClosed.of_valuativeCriterion (pullback.diagonal f) h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
⊢ IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)
have suffices : ValuativeCriterion.Existence (Y := pullback.diagonalObj f) (pullback.diagonal f)
Tactic: suffices h : ValuativeCriterion.Existence (pullback.diagonal f) by
      have := UniversallyClosed.of_valuativeCriterion (pullback.diagonal f) h
      exact .of_isPreimmersion _ (pullback.diagonal f).isClosedMap.isClosed_range
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ ⋯.HasLift
have hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
Tactic: have hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))
        f (S.i₂ ≫ pullback.fst f f ≫ f) := ⟨by simp [← S.commSq.w_assoc]⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
⊢ ⋯.HasLift
have this : Subsingleton.{u + 1} sorry.LiftStruct
Tactic: have : Subsingleton S'.commSq.LiftStruct := hf S'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
⊢ ⋯.HasLift
have h₁₂ : S'l₁ = S'l₂
Tactic: have h₁₂ : S'l₁ = S'l₂ := Subsingleton.elim _ _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ ⋯.HasLift
have exists_lift : Nonempty.{u + 1} sorry.LiftStruct
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ Nonempty.{u + 1} ⋯.LiftStruct
have exists_lift : sorry.LiftStruct
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ ⋯.LiftStruct
have exists_lift : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁
Tactic: refine ⟨S.i₂ ≫ pullback.fst _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
exists_lift : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁
⊢ ⋯.LiftStruct
have exists_lift₁ : (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂
Tactic: refine ⟨S.i₂ ≫ pullback.fst _ _, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂
have exists_lift : S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f = S.i₂
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f = S.i₂
have exists_lift : CategoryStruct.comp (Y := pullback f f) (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) (pullback.fst f f) =
  S.i₂ ≫ pullback.fst f f
Tactic: apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
exists_lift :
  CategoryStruct.comp (Y := pullback f f) (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) (pullback.fst f f) =
    S.i₂ ≫ pullback.fst f f
⊢ S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f = S.i₂
have exists_lift₁ : CategoryStruct.comp (Y := pullback f f) (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) (pullback.snd f f) =
  S.i₂ ≫ pullback.snd f f
Tactic: apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
hc : CommSq S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) f (S.i₂ ≫ pullback.fst f f ≫ f)
S' : ValuativeCommSq f :=
  { R := S.R, commRing := S.commRing, domain := ⋯, valuationRing := ⋯, K := S.K, field := S.field, algebra := S.algebra,
    isFractionRing := ⋯, i₁ := S.i₁, i₂ := S.i₂ ≫ pullback.fst f f ≫ f, commSq := hc }
this : Subsingleton.{u + 1} ⋯.LiftStruct
S'l₁ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.fst f f, fac_left := ⋯, fac_right := ⋯ }
S'l₂ : ⋯.LiftStruct := { l := S.i₂ ≫ pullback.snd f f, fac_left := ⋯, fac_right := ⋯ }
h₁₂ : S'l₁ = S'l₂
⊢ CategoryStruct.comp (Y := pullback f f) (S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f) (pullback.snd f f) =
    S.i₂ ≫ pullback.snd f f
have exists_lift : S.i₂ ≫ pullback.fst f f = S.i₂ ≫ pullback.snd f f
Tactic: simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSeparated f
S : ValuativeCommSq f
⊢ Subsingleton.{u + 1} ⋯.LiftStruct
have allEq : ∀ (a b : sorry.LiftStruct), a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
⊢ Eq (α := ⋯.LiftStruct) { l := l₁, fac_left := hl₁, fac_right := hl₁' } { l := l₂, fac_left := hl₂, fac_right := hl₂' }
have allEq : CommSq.LiftStruct.l (sq := sorry) { l := l₁, fac_left := hl₁, fac_right := hl₁' : sorry.LiftStruct } =
  CommSq.LiftStruct.l (sq := sorry) { l := l₂, fac_left := hl₂, fac_right := hl₂' }
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
⊢ CommSq.LiftStruct.l (sq := ⋯) { l := l₁, fac_left := hl₁, fac_right := hl₁' : ⋯.LiftStruct } =
    CommSq.LiftStruct.l (sq := ⋯) { l := l₂, fac_left := hl₂, fac_right := hl₂' }
have allEq : l₁ = l₂
Tactic: dsimp at *
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
⊢ l₁ = l₂
have h : l₁ ≫ f = l₂ ≫ f
Tactic: have h := hl₁'.trans hl₂'.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSeparated f
S : ValuativeCommSq f
l₁ : Spec (CommRingCat.of S.R) ⟶ X
hl₁ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₁ = S.i₁
hl₁' : l₁ ≫ f = S.i₂
l₂ : Spec (CommRingCat.of S.R) ⟶ X
hl₂ : Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ l₂ = S.i₁
hl₂' : l₂ ≫ f = S.i₂
h : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (Z := pullback.diagonalObj f) (pullback.diagonal f) (pullback.lift l₁ l₂ h)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h)
⊢ l₁ = l₂
have this : IsClosedImmersion g
Tactic: have : IsClosedImmersion g := MorphismProperty.pullback_snd _ _ inferInstance