no goals
K : Type ?u.2929625
F : Type ?u.2929628
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type u_3
Γ''₀ : Type ?u.2929643
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h : IsEquiv v₁ v₂
r s : R
⊢ ↑v₁ r = ↑v₁ s ↔ ↑v₂ r = ↑v₂ s
simpa only [le_antisymm_iff] using and_congr (h r s) (h s r)