case tfae_1_iff_2
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1

K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
tfae_have 1 ↔ 2
case tfae_1_iff_3
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1

K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
tfae_have 1 ↔ 3
case tfae_1_iff_4
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1

K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
tfae_have 1 ↔ 4
case tfae_1_iff_5
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1

K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
tfae_1_iff_5 : IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
tfae_have 1 ↔ 5
no goals
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
tfae_1_iff_5 : IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
⊢ List.TFAE
    [IsEquiv v v', ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1, ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1, ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1,
      ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1]
tfae_finish
no goals
case tfae_1_iff_2
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
apply isEquiv_iff_val_le_one
no goals
case tfae_1_iff_3
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
apply isEquiv_iff_val_eq_one
no goals
case tfae_1_iff_4
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
apply isEquiv_iff_val_lt_one
no goals
case tfae_1_iff_5
K : Type u_3
F : Type ?u.3476375
R : Type ?u.3476378
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3476390
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x ≤ 1 ↔ ↑v' x ≤ 1
tfae_1_iff_3 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x = 1 ↔ ↑v' x = 1
tfae_1_iff_4 : IsEquiv v v' ↔ ∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
apply isEquiv_iff_val_sub_one_lt_one