normal form for abs value associated to an infinite place

Stream: mathlib4

[Kevin Buzzard]

We have

def NumberField.InfinitePlace := { w : AbsoluteValue K ℝ // ∃ φ : K →+* ℂ, place φ = w }

and if v : InfinitePlace K then one can use v.1 or v.val to refer to the absolute value. These are both displayed as ↑v, but actually using ↑v in code doesn't seem to work, presumably because defs are irreducible nowadays. Should I add a coercion, make the def reducible or do nothing? I'm a bit unclear about the consequences of these choices.

[Daniel Weber]

Another option is using a new structure instead of subtype, I think that's usually preferred (although I don't remember the reasons for that)