∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  {x : R} {g : MonoidWithZeroHom.ValueGroup₀ v}, v.restrict x ≤ g ↔ v x ≤ MonoidWithZeroHom.ValueGroup₀.embedding g