awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact this.left

Premises used: And.left
-- 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

Tactic:
have hZ : IsAffine Z := by
    rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
    exact this.left
-- 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_1 : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
rw : g ≫ l₁ = g ≫ l₂
⊢ l₁ = l₂

Tactic:
rw [← cancel_epi g]

Premises used: CategoryTheory.cancel_epi
-- 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_1 : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
rw :
  pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
    CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.fst f f)
| g ≫ l₁

Tactic:
rw [← pullback.lift_fst l₁ l₂ h, ← pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pullback.lift_fst
-- 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_1 : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
conv_lhs :
  pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
      CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.fst f f) =
    g ≫ l₂
⊢ g ≫ l₁ = g ≫ l₂

Tactic:
conv_lhs => rw [← pullback.lift_fst l₁ l₂ h, ← pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pullback.lift_fst
-- 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_1 : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
rw :
  pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
    CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.snd f f)
| g ≫ l₂

Tactic:
rw [← pullback.lift_snd l₁ l₂ h, ← pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullback.condition_assoc
-- 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_1 : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
conv_rhs :
  Eq (α := Z ⟶ X)
    (pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
      CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.fst f f))
    (pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
      CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.snd f f))
⊢ pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
      CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.fst f f) =
    g ≫ l₂

Tactic:
conv_rhs => rw [← pullback.lift_snd l₁ l₂ h, ← pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.lift_snd, CategoryTheory.Limits.pullback.condition_assoc
-- 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_1 : IsClosedImmersion g
hZ : IsAffine Z
this : IsIso g
⊢ Eq (α := Z ⟶ X)
    (pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
      CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.fst f f))
    (pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
      CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.snd f f))

Tactic:
simp
-- 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
hZ : IsAffine Z
allEq : IsIso g
⊢ l₁ = l₂

Tactic:
suffices IsIso g by
    rw [← cancel_epi g]
    conv_lhs => rw [← pullback.lift_fst l₁ l₂ h, ← pullback.condition_assoc]
    conv_rhs => rw [← pullback.lift_snd l₁ l₂ h, ← pullback.condition_assoc]
    simp
-- 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_1 : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (Z := pullback.diagonalObj f) (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
this : IsClosedImmersion g
hZ : IsAffine Z
h :
  Function.Bijective (α := (↑Γ(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))
⊢ IsIso g

Tactic:
(HasAffineProperty.iff_of_isAffine (P := MorphismProperty.isomorphisms Scheme)).mpr ?_

Premises used: Iff.mpr, 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_1 : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (Z := pullback.diagonalObj f) (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
this : IsClosedImmersion g
hZ : IsAffine Z
h :
  Function.Bijective (α := (↑Γ(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))
refine : IsAffine Z ∧ IsIso (Scheme.Hom.appTop g)
⊢ IsIso g

Tactic:
refine (HasAffineProperty.iff_of_isAffine (P := MorphismProperty.isomorphisms Scheme)).mpr ?_

Premises used: Iff.mpr, 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_1 : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (Z := pullback.diagonalObj f) (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
this : IsClosedImmersion g
hZ : IsAffine Z
h :
  Function.Bijective (α := (↑Γ(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 ∧ IsIso (Scheme.Hom.appTop g)

Tactic:
⟨hZ, (ConcreteCategory.isIso_iff_bijective _).mpr h⟩

Premises used: Iff.mpr, CategoryTheory.ConcreteCategory.isIso_iff_bijective, And.intro
-- 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_1 : l₁ ≫ f = l₂ ≫ f
Z : Scheme := pullback (Z := pullback.diagonalObj f) (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
g : Z ⟶ Spec (CommRingCat.of S.R) := pullback.snd (pullback.diagonal f) (pullback.lift l₁ l₂ h_1)
this : IsClosedImmersion g
hZ : IsAffine Z
h :
  Function.Bijective (α := (↑Γ(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 ∧ IsIso (Scheme.Hom.appTop g)

Tactic:
exact ⟨hZ, (ConcreteCategory.isIso_iff_bijective _).mpr h⟩
-- 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
hZ : IsAffine Z
allEq :
  Function.Bijective (α := (↑Γ(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))
⊢ IsIso g

Tactic:
suffices h : Function.Bijective (g.appTop) by
    refine (HasAffineProperty.iff_of_isAffine (P := MorphismProperty.isomorphisms Scheme)).mpr ?_
    exact ⟨hZ, (ConcreteCategory.isIso_iff_bijective _).mpr h⟩
-- 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
hZ : IsAffine Z
allEq :
  Function.Injective (α := (↑Γ(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))
allEq₁ :
  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))
⊢ Function.Bijective (α := (↑Γ(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:
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₂
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
hZ : IsAffine Z
h₀ :
  CategoryStruct.comp (Y := pullback f f) (S.i₁ ≫ pullback.diagonal f) (pullback.fst f f) =
    CategoryStruct.comp (Y := pullback f f) (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h)
      (pullback.fst f f)
h₁ :
  CategoryStruct.comp (Y := pullback f f) (S.i₁ ≫ pullback.diagonal f) (pullback.snd f f) =
    CategoryStruct.comp (Y := pullback f f) (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h)
      (pullback.snd f f)
⊢ Eq (α := Spec (CommRingCat.of S.K) ⟶ pullback.diagonalObj f) (S.i₁ ≫ pullback.diagonal f)
    (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h)

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 : 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
hZ : IsAffine Z
⊢ CategoryStruct.comp (Y := pullback f f) (S.i₁ ≫ pullback.diagonal f) (pullback.fst f f) =
    CategoryStruct.comp (Y := pullback f f) (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h)
      (pullback.fst f f)

Tactic:
simpa using hl₁.symm

Premises used: Eq.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)
this : IsClosedImmersion g
hZ : IsAffine Z
⊢ CategoryStruct.comp (Y := pullback f f) (S.i₁ ≫ pullback.diagonal f) (pullback.snd f f) =
    CategoryStruct.comp (Y := pullback f f) (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) ≫ pullback.lift l₁ l₂ h)
      (pullback.snd f f)

Tactic:
simpa using hl₂.symm

Premises used: Eq.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)
this : IsClosedImmersion g
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
⊢ l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))

Tactic:
have hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)) :=
      pullback.lift_snd _ _ _
-- 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
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
rw :
  Function.Injective (α := (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) (β :=
    (↑Γ(Spec (CommRingCat.of S.K), ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(Spec (CommRingCat.of S.R), ⊤)) (Y := Γ(Spec (CommRingCat.of S.K), ⊤))
          (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))))) :
      (a : (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) → (↑Γ(Spec (CommRingCat.of S.K), ⊤) : Type u))
⊢ Function.Injective (α := (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) (β :=
    (↑Γ(Spec (CommRingCat.of S.K), ⊤) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appTop (l ≫ g))) :
      (a : (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) → (↑Γ(Spec (CommRingCat.of S.K), ⊤) : Type u))

Tactic:
rw [hg]
-- 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
hZ : IsAffine Z
l : Spec (CommRingCat.of S.K) ⟶ Z := pullback.lift S.i₁ (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))) ⋯
hg : l ≫ g = Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))
e : Arrow.mk (X := CommRingCat.of S.R) (Y := CommRingCat.of S.K) (CommRingCat.ofHom (algebraMap S.R S.K)) ≅
  Arrow.mk (X := Γ(Spec (CommRingCat.of S.R), ⊤)) (Y := Γ(Spec (CommRingCat.of S.K), ⊤))
    (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K)))) :=
  arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom (algebraMap S.R S.K))
P : MorphismProperty CommRingCat :=
  RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
    Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)
⊢ (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)).RespectsIso

Tactic:
have : (RingHom.toMorphismProperty <| fun f ↦ Function.Injective f).RespectsIso :=
        RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.injective_respectsIso