case tfae_1_iff_2
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹

R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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⁻¹
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
tfae_have 1 ↔ 2
case tfae_1_iff_3
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 ↔ IsTotal R fun x x_1 => x ∣ x_1

R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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⁻¹
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
tfae_have 1 ↔ 3
case tfae_1_iff_4
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
⊢ ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1

R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
tfae_have 1 ↔ 4
case tfae_1_iff_5
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
⊢ ValuationRing R ↔ LocalRing R ∧ IsBezout R

R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
tfae_1_iff_5 : ValuationRing R ↔ LocalRing R ∧ IsBezout R
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
tfae_have 1 ↔ 5
no goals
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
tfae_1_iff_5 : ValuationRing R ↔ LocalRing R ∧ IsBezout R
⊢ List.TFAE
    [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹,
      IsTotal R fun x x_1 => x ∣ x_1, IsTotal (Ideal R) fun x x_1 => x ≤ x_1, LocalRing R ∧ IsBezout R]
tfae_finish
no goals
case tfae_1_iff_2
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ ValuationRing R ↔ ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹
exact iff_isInteger_or_isInteger R _
no goals
case tfae_1_iff_3
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 ↔ IsTotal R fun x x_1 => x ∣ x_1
exact iff_dvd_total
no goals
case tfae_1_iff_4
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
⊢ ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
exact iff_ideal_total
no goals
case tfae_1_iff_5
R✝ : Type ?u.597723
inst✝⁶ : CommRing R✝
inst✝⁵ : IsDomain R✝
K : Type ?u.597912
inst✝⁴ : Field K
inst✝³ : Algebra R✝ K
inst✝² : IsFractionRing R✝ K
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 x x_1 => x ∣ x_1
tfae_1_iff_4 : ValuationRing R ↔ IsTotal (Ideal R) fun x x_1 => x ≤ x_1
⊢ ValuationRing R ↔ LocalRing R ∧ IsBezout R
exact iff_local_bezout_domain