-- Mathlib/RingTheory/Valuation/ValuationRing.lean
theorem TFAE (R : Type u) [CommRing R] [IsDomain R] :
    List.TFAE
      [ValuationRing R,
        ∀ x : FractionRing R, IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
        IsTotal R (· ∣ ·), IsTotal (Ideal R) (· ≤ ·), IsLocalRing R ∧ IsBezout R]

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_have 1 ↔ 3 := iff_dvd_total

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ IsTotal R fun x1 x2 => x1 ∣ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ IsTotal R fun x1 x2 => x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_have 1 ↔ 5 := iff_local_bezout_domain

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ IsTotal R fun x1 x2 => x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
tfae_1_iff_5 : ValuationRing R ↔ IsLocalRing R ∧ IsBezout R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ IsTotal R fun x1 x2 => x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
tfae_1_iff_5 : ValuationRing R ↔ IsLocalRing R ∧ IsBezout R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ IsTotal R fun x1 x2 => x1 ∣ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_have 1 ↔ 4 := iff_ideal_total

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
tfae_1_iff_3 : ValuationRing R ↔ IsTotal R fun x1 x2 => x1 ∣ x2
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE

Tactic:
tfae_have 1 ↔ 2 := iff_isInteger_or_isInteger R _

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
tfae_1_iff_2 : ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
⊢ [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x1 x2 => x1 ∣ x2, IsTotal (Ideal R) fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE