K : Type u_3
F : Type ?u.3433435
R : Type ?u.3433438
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3433450
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {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.3433435
R : Type ?u.3433438
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3433450
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ IsEquiv v v' ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
rw [isEquiv_iff_val_lt_one]
no goals
K : Type u_3
F : Type ?u.3433435
R : Type ?u.3433438
inst✝³ : DivisionRing K
Γ₀ : Type u_1
Γ'₀ : Type u_2
Γ''₀ : Type ?u.3433450
inst✝² : LinearOrderedCommMonoidWithZero Γ''₀
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
⊢ (∀ {x : K}, ↑v x < 1 ↔ ↑v' x < 1) ↔ ∀ {x : K}, ↑v (x - 1) < 1 ↔ ↑v' (x - 1) < 1
exact (Equiv.subRight 1).surjective.forall