no goals
K : Type ?u.71899
F : Type ?u.71902
R : Type u_1
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.71914
Γ''₀ : Type ?u.71917
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
⊢ ↑v.toMonoidWithZeroHom = ↑v
rfl