awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
rw : (topologically @SpecializingMap).universally ⊓ @QuasiCompact = ValuativeCriterion.Existence ⊓ @QuasiCompact
rw₁ rw₂ :
  (topologically @SpecializingMap).universally ⊓ @QuasiCompact =
    (topologically @SpecializingMap).universally ⊓ @QuasiCompact
⊢ @UniversallyClosed = ValuativeCriterion.Existence ⊓ @QuasiCompact

Tactic:
rw [universallyClosed_eq_universallySpecializing, ValuativeCriterion.Existence.eq]

Premises used: AlgebraicGeometry.ValuativeCriterion.Existence.eq, AlgebraicGeometry.universallyClosed_eq_universallySpecializing
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
hf : ValuativeCriterion.Existence f
rw : (ValuativeCriterion.Existence ⊓ @QuasiCompact) f
⊢ UniversallyClosed f

Tactic:
rw [eq_valuativeCriterion]

Premises used: AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ (ValuativeCriterion.Existence ⊓ @QuasiCompact) f

Tactic:
⟨hf, ‹_›⟩

Premises used: And.intro
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
hf : ValuativeCriterion.Existence f
⊢ (ValuativeCriterion.Existence ⊓ @QuasiCompact) f

Tactic:
exact ⟨hf, ‹_›⟩
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ UniversallyClosed (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
have := UniversallyClosed.of_valuativeCriterion (pullback.diagonal f) h
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (Y := pullback.diagonalObj f) (pullback.diagonal f)
this : UniversallyClosed (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
.of_isPreimmersion _ (pullback.diagonal f).isClosedMap.isClosed_range

Premises used: AlgebraicGeometry.IsClosedImmersion.of_isPreimmersion, AlgebraicGeometry.Scheme.Hom.isClosedMap, CategoryTheory.Limits.pullback.diagonal, IsClosedMap.isClosed_range
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
h : ValuativeCriterion.Existence (Y := pullback.diagonalObj f) (pullback.diagonal f)
this : UniversallyClosed (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsClosedImmersion (Y := pullback.diagonalObj f) (pullback.diagonal f)

Tactic:
exact .of_isPreimmersion _ (pullback.diagonal f).isClosedMap.isClosed_range
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
suffices : ValuativeCriterion.Existence (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ IsClosedImmersion (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
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ S.i₁ ≫ f = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f ≫ f

Tactic:
simp [← S.commSq.w_assoc]

Premises used: AlgebraicGeometry.ValuativeCommSq.commSq, CategoryTheory.CommSq.w_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
hf : ValuativeCriterion.Uniqueness f
S : ValuativeCommSq (Y := pullback.diagonalObj f) (pullback.diagonal f)
⊢ 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]⟩
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 }
⊢ Subsingleton.{u + 1} ⋯.LiftStruct

Tactic:
have : Subsingleton S'.commSq.LiftStruct := hf S'
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
⊢ Spec.map (CommRingCat.ofHom (algebraMap S'.R S'.K)) ≫ S.i₂ ≫ pullback.fst f f = S'.i₁

Tactic:
simp [S', ← S.commSq.w_assoc]

Premises used: AlgebraicGeometry.ValuativeCommSq.commSq, CategoryTheory.CommSq.w_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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.i₂ ≫ pullback.fst f f) ≫ f = S'.i₂

Tactic:
simp [S']
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 := ⋯ }
⊢ Spec.map (CommRingCat.ofHom (algebraMap S'.R S'.K)) ≫ S.i₂ ≫ pullback.snd f f = S'.i₁

Tactic:
simp [S', ← S.commSq.w_assoc]

Premises used: AlgebraicGeometry.ValuativeCommSq.commSq, CategoryTheory.CommSq.w_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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.i₂ ≫ pullback.snd f f) ≫ f = S'.i₂

Tactic:
simp [S', pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 := ⋯ }
⊢ S'l₁ = S'l₂

Tactic:
have h₁₂ : S'l₁ = S'l₂ := Subsingleton.elim _ _
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 : Nonempty.{u + 1} ⋯.LiftStruct
⊢ ⋯.HasLift

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 : ⋯.LiftStruct
⊢ Nonempty.{u + 1} ⋯.LiftStruct

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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₁
exists_lift₁ : (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂
⊢ ⋯.LiftStruct

Tactic:
refine ⟨S.i₂ ≫ pullback.fst _ _, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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₂
⊢ Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ S.i₂ ≫ pullback.fst f f = S.i₁

Tactic:
simp [← S.commSq.w_assoc]

Premises used: AlgebraicGeometry.ValuativeCommSq.commSq, CategoryTheory.CommSq.w_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 : S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f = S.i₂
⊢ (S.i₂ ≫ pullback.fst f f) ≫ pullback.diagonal f = S.i₂

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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
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
⊢ S.i₂ ≫ pullback.fst f f ≫ pullback.diagonal f = S.i₂

Tactic:
apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)

Premises used: CategoryTheory.IsPullback.hom_ext, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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.fst f f) =
    S.i₂ ≫ pullback.fst f f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 : S.i₂ ≫ pullback.fst f f = S.i₂ ≫ pullback.snd f f
⊢ 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:
simp only [Category.assoc, pullback.diagonal_snd, Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.diagonal_snd, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 = S.i₂ ≫ pullback.snd f f

Tactic:
congrArg CommSq.LiftStruct.l h₁₂

Premises used: congrArg, CategoryTheory.CommSq.LiftStruct.l
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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 = S.i₂ ≫ pullback.snd f f

Tactic:
exact congrArg CommSq.LiftStruct.l h₁₂

Premises used: congrArg, CategoryTheory.CommSq.LiftStruct.l
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsSeparated f
S : ValuativeCommSq f
allEq : ∀ (a b : ⋯.LiftStruct), a = b
⊢ Subsingleton.{u + 1} ⋯.LiftStruct

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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₂
allEq :
  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₂' }
⊢ Eq (α := ⋯.LiftStruct) { l := l₁, fac_left := hl₁, fac_right := hl₁' } { l := l₂, fac_left := hl₂, fac_right := hl₂' }

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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₂
allEq : l₁ = l₂
⊢ 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₂' }

Tactic:
dsimp at *
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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₁ ≫ f = l₂ ≫ f

Tactic:
have h := hl₁'.trans hl₂'.symm
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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)
⊢ IsClosedImmersion g

Tactic:
have : IsClosedImmersion g := MorphismProperty.pullback_snd _ _ inferInstance
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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)
this : IsClosedImmersion g
⊢ IsAffine Z ∧
    Function.Surjective (α := (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) (β := (↑Γ(Z, ⊤) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop g)) :
        (a : (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) → (↑Γ(Z, ⊤) : Type u))

Tactic:
rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
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)
this :
  IsAffine Z ∧
    Function.Surjective (α := (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) (β := (↑Γ(Z, ⊤) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop g)) :
        (a : (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) → (↑Γ(Z, ⊤) : Type u))
⊢ IsAffine Z

Tactic:
this.left

Premises used: And.left