awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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))))
have rw : P (X := CommRingCat.of S.R) (Y := CommRingCat.of S.K) (CommRingCat.ofHom (algebraMap S.R S.K))
Tactic: rw [← MorphismProperty.arrow_mk_iso_iff (P := P) e]
-- 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))
⊢ 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 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))
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
-- 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_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)) (β := (↑Γ(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 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))
Tactic: rw [Scheme.Hom.comp_appTop] 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
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))
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, hZ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
⊢ @IsSeparated = ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated
have h : ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y), IsSeparated f ↔ (ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
⊢ @IsProper = ValuativeCriterion ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType
have rw : ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
    @LocallyOfFiniteType =
  ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓ @LocallyOfFiniteType
Tactic: rw [isProper_eq, IsSeparated.eq_valuativeCriterion, ValuativeCriterion.eq,
    UniversallyClosed.eq_valuativeCriterion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
⊢ ValuativeCriterion.Uniqueness ⊓ @QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ @QuasiCompact) ⊓
      @LocallyOfFiniteType =
    ValuativeCriterion.Existence ⊓ ValuativeCriterion.Uniqueness ⊓ @QuasiCompact ⊓ @QuasiSeparated ⊓
      @LocallyOfFiniteType
have simp_rw : ValuativeCriterion.Uniqueness ⊓
    (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))) =
  ValuativeCriterion.Existence ⊓
    (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType)))
Tactic: simp_rw [inf_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
⊢ ValuativeCriterion.Uniqueness ⊓
      (@QuasiSeparated ⊓ (ValuativeCriterion.Existence ⊓ (@QuasiCompact ⊓ @LocallyOfFiniteType))) =
    ValuativeCriterion.Existence ⊓
      (ValuativeCriterion.Uniqueness ⊓ (@QuasiCompact ⊓ (@QuasiSeparated ⊓ @LocallyOfFiniteType)))
have 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
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h : ValuativeCriterion.Uniqueness f ∧
    QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
  ValuativeCriterion.Existence f ∧
    ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₁ : ValuativeCriterion.Existence f ∧
    ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
  ValuativeCriterion.Uniqueness f ∧
    QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₂ : ValuativeCriterion.Uniqueness f →
  QuasiSeparated f →
    ValuativeCriterion.Existence f →
      QuasiCompact f →
        LocallyOfFiniteType f →
          ValuativeCriterion.Existence f ∧
            ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₂ h₃ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f →
        QuasiCompact f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Existence f ∧
              ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₄ : ValuativeCriterion.Uniqueness f →
  QuasiSeparated f →
    ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₂ h₃ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f →
        QuasiCompact f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Existence f ∧
              ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₄ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₅ : ValuativeCriterion.Uniqueness f →
  QuasiSeparated f →
    ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₂ h₃ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f →
        QuasiCompact f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Existence f ∧
              ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₄ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
h₅ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₆ : ValuativeCriterion.Uniqueness f →
  QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiCompact f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₂ h₃ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f →
        QuasiCompact f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Existence f ∧
              ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₄ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
h₅ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
h₆ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiCompact f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₇ : ValuativeCriterion.Uniqueness f →
  QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiSeparated f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₂ h₃ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f →
        QuasiCompact f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Existence f ∧
              ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₄ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
h₅ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
h₆ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiCompact f
h₇ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiSeparated f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₈ : ValuativeCriterion.Uniqueness f →
  QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → LocallyOfFiniteType f
Tactic: tauto
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ValuativeCriterion (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₁ :
  ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f →
    ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
h₂ h₃ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f →
        QuasiCompact f →
          LocallyOfFiniteType f →
            ValuativeCriterion.Existence f ∧
              ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
h₄ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
h₅ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f →
      ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
h₆ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiCompact f
h₇ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → QuasiSeparated f
h₈ :
  ValuativeCriterion.Uniqueness f →
    QuasiSeparated f → ValuativeCriterion.Existence f → QuasiCompact f → LocallyOfFiniteType f → LocallyOfFiniteType f
⊢ ValuativeCriterion.Uniqueness f ∧
      QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f ↔
    ValuativeCriterion.Existence f ∧
      ValuativeCriterion.Uniqueness f ∧ QuasiCompact f ∧ QuasiSeparated f ∧ LocallyOfFiniteType f
have h₉ : ValuativeCriterion.Existence f →
  ValuativeCriterion.Uniqueness f →
    QuasiCompact f →
      QuasiSeparated f →
        LocallyOfFiniteType f →
          ValuativeCriterion.Uniqueness f ∧
            QuasiSeparated f ∧ ValuativeCriterion.Existence f ∧ QuasiCompact f ∧ LocallyOfFiniteType f
Tactic: tauto