-- 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
h₉ 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₁₁ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f →
      QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → ValuativeCriterion.Uniqueness f
h₁₂ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f → QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → QuasiSeparated f
h₁₃ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f →
      QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → ValuativeCriterion.Existence f
h₁₄ :
  ValuativeCriterion.Existence f →
    ValuativeCriterion.Uniqueness f → QuasiCompact f → QuasiSeparated 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.Existence f →
  ValuativeCriterion.Uniqueness f → QuasiCompact f → QuasiSeparated f → LocallyOfFiniteType f → LocallyOfFiniteType f
Tactic: tauto