awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
this : IsClosedImmersion g
⊢ IsAffine Z
have 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))
Tactic: rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
Cleared hypotheses: this
-- 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)
this : IsClosedImmersion g
⊢ l₁ = l₂
have hZ : IsAffine Z
Tactic: have hZ : IsAffine Z := by
    rw [@HasAffineProperty.iff_of_isAffine @IsClosedImmersion] at this
    exact this.left
-- 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₂
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
⊢ l₁ = l₂
have rw : g ≫ l₁ = g ≫ l₂
Tactic: rw [← cancel_epi g]
-- 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₂
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
| g ≫ l₁
have rw : pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
  CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.fst f f)
Tactic: rw [← pullback.lift_fst l₁ l₂ h, ← pullback.condition_assoc]
-- 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₂
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
⊢ g ≫ l₁ = g ≫ l₂
have 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₂
Tactic: conv_lhs => rw [← pullback.lift_fst l₁ l₂ h, ← pullback.condition_assoc]
-- 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₂
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
| g ≫ l₂
have rw : pullback.fst (pullback.diagonal f) (pullback.lift l₁ l₂ h) ≫
  CategoryStruct.comp (Y := pullback.diagonalObj f) (pullback.diagonal f) (pullback.snd f f)
Tactic: rw [← pullback.lift_snd l₁ l₂ h, ← pullback.condition_assoc]
-- 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₂
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
⊢ 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₂
have 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))
Tactic: conv_rhs => rw [← pullback.lift_snd l₁ l₂ h, ← pullback.condition_assoc]
-- 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₂
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₁ = l₂
have allEq : IsIso g
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
-- 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₂
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
have refine : IsAffine Z ∧ IsIso (Scheme.Hom.appTop g)
Tactic: refine (HasAffineProperty.iff_of_isAffine (P := MorphismProperty.isomorphisms Scheme)).mpr ?_
-- 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₂
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
⊢ IsIso g
have 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))
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⟩
-- 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₂
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
⊢ 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))
have 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))
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₂
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))
⊢ 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))
have 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))
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₂
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
⊢ 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)
have 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)
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 : 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)
⊢ 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)
have 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)
Tactic: apply IsPullback.hom_ext (IsPullback.of_hasPullback _ _)
-- 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)
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))) ⋯
⊢ 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))
have hg : 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 _ _ _
-- 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₂
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))
⊢ 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))
have 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))
Tactic: rw [hg]
-- 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)
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)
⊢ 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))
have this₁ : (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
-- 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₂
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
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)
this :
  (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
      Function.Injective (α := R) (β := S) (⇑f : (a : R) → S)).RespectsIso
⊢ 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))
have change : P (X := Γ(Spec (CommRingCat.of S.R), ⊤)) (Y := Γ(Spec (CommRingCat.of S.K), ⊤))
  (Scheme.Hom.appTop (Spec.map (CommRingCat.ofHom (algebraMap S.R S.K))))
Tactic: change P _