∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  {γ : Γ₀ˣ}, {x | Valued.extensionValuation x < ↑γ} = closure (UniformSpace.Completion.coe' '' {x | Valued.v x < ↑γ})