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_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
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))))
⊢ 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:
change P _
-- 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
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
rw : P (X := CommRingCat.of S.R) (Y := CommRingCat.of S.K) (CommRingCat.ofHom (algebraMap S.R S.K))
⊢ 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:
rw [← MorphismProperty.arrow_mk_iso_iff (P := P) e]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- 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
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
⊢ P (X := CommRingCat.of S.R) (Y := CommRingCat.of S.K) (CommRingCat.ofHom (algebraMap S.R S.K))

Tactic:
FaithfulSMul.algebraMap_injective S.R S.K

Premises used: FaithfulSMul.algebraMap_injective, RingHom.toMorphismProperty, AlgebraicGeometry.ValuativeCommSq.R, AlgebraicGeometry.ValuativeCommSq.K
-- 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
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
⊢ P (X := CommRingCat.of S.R) (Y := CommRingCat.of S.K) (CommRingCat.ofHom (algebraMap S.R S.K))

Tactic:
exact FaithfulSMul.algebraMap_injective S.R S.K

Premises used: FaithfulSMul.algebraMap_injective, AlgebraicGeometry.ValuativeCommSq.R, AlgebraicGeometry.ValuativeCommSq.K
-- 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))
⊢ 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:
have : Function.Injective ((l ≫ g).appTop) := by
      rw [hg]
      let e := arrowIsoΓSpecOfIsAffine (CommRingCat.ofHom <| algebraMap S.R S.K)
      let P : MorphismProperty CommRingCat :=
        RingHom.toMorphismProperty <| fun f ↦ Function.Injective f
      have : (RingHom.toMorphismProperty <| fun f ↦ Function.Injective f).RespectsIso :=
        RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.injective_respectsIso
      change P _
      rw [← MorphismProperty.arrow_mk_iso_iff (P := P) e]
      exact FaithfulSMul.algebraMap_injective S.R S.K
-- 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
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))
this :
  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))
⊢ 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 g ≫ Scheme.Hom.appTop l)) :
      (a : (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) → (↑Γ(Spec (CommRingCat.of S.K), ⊤) : Type u))

Tactic:
rw [Scheme.Hom.comp_appTop] at this

Premises used: AlgebraicGeometry.Scheme.Hom.comp_appTop
-- 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
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))
this :
  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 g ≫ Scheme.Hom.appTop l)) :
      (a : (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) → (↑Γ(Spec (CommRingCat.of S.K), ⊤) : Type u))
⊢ 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:
Function.Injective.of_comp this

Premises used: Function.Injective.of_comp
-- 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
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))
this :
  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 g ≫ Scheme.Hom.appTop l)) :
      (a : (↑Γ(Spec (CommRingCat.of S.R), ⊤) : Type u)) → (↑Γ(Spec (CommRingCat.of S.K), ⊤) : Type u))
⊢ 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:
exact Function.Injective.of_comp this

Premises used: Function.Injective.of_comp
-- 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
⊢ 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 : IsClosedImmersion g
hZ : IsAffine Z
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:
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))
hZ : 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:
this.right

Premises used: And.right
-- 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))
hZ : 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:
exact this.right

Premises used: And.right
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y), IsSeparated f ↔ (ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated) f
⊢ @IsSeparated = ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsSeparated f ↔ (ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated) f

Tactic:
⟨fun _ ↦ ⟨IsSeparated.valuativeCriterion f, inferInstance⟩,
    fun ⟨H, _⟩ ↦ .of_valuativeCriterion f H⟩

Premises used: inferInstance, AlgebraicGeometry.IsSeparated.valuativeCriterion, AlgebraicGeometry.IsSeparated.of_valuativeCriterion, And.intro, Iff.intro, AlgebraicGeometry.IsSeparated, _private.0.AlgebraicGeometry.IsSeparated.eq_valuativeCriterion.match_1
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ IsSeparated f ↔ (ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated) f

Tactic:
exact ⟨fun _ ↦ ⟨IsSeparated.valuativeCriterion f, inferInstance⟩,
    fun ⟨H, _⟩ ↦ .of_valuativeCriterion f H⟩
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
rw :
  ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
      @LocallyOfFiniteType =
    ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓
      @LocallyOfFiniteType
⊢ @IsProper = ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType

Tactic:
rw [isProper_eq, IsSeparated.eq_valuativeCriterion, ValuativeCriterion.eq,
    UniversallyClosed.eq_valuativeCriterion]

Premises used: AlgebraicGeometry.IsSeparated.eq_valuativeCriterion, AlgebraicGeometry.isProper_eq, AlgebraicGeometry.UniversallyClosed.eq_valuativeCriterion, AlgebraicGeometry.ValuativeCriterion.eq
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
simp_rw :
  ValuativeCriterion.Uniqueness ⊓
      (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))) =
    ValuativeCriterion.Existence ⊓
      (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType)))
⊢ ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
      @LocallyOfFiniteType =
    ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓
      @LocallyOfFiniteType

Tactic:
simp_rw [inf_assoc]

Premises used: inf_assoc
-- Module: Mathlib.AlgebraicGeometry.ValuativeCriterion
Goal:
h :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y),
    (ValuativeCriterion.Uniqueness ⊓
          (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))))
        f ↔
      (ValuativeCriterion.Existence ⊓
          (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType))))
        f
⊢ ValuativeCriterion.Uniqueness ⊓
      (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))) =
    ValuativeCriterion.Existence ⊓
      (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType)))

Tactic:
ext X Y f