K : Type ?u.2583538
F : Type ?u.2583541
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.2583553
Γ''₀ : Type ?u.2583556
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
⊢ IsEquiv v v
K : Type ?u.2583538
F : Type ?u.2583541
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.2583553
Γ''₀ : Type ?u.2583556
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
v' : Valuation R Γ₀
h : v = v'
⊢ IsEquiv v v'
subst h
no goals
K : Type ?u.2583538
F : Type ?u.2583541
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.2583553
Γ''₀ : Type ?u.2583556
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
⊢ IsEquiv v v
rfl