How to get subtype element

Stream: lean4

[Mathias Schack Rabing]

Hi if I e.g. have (p (n : ℕ): Prop := n ≠ 0). How do i then get from an element (n : ℕ) where (n ≠ 0) get the corresponding element in (subtype p).
Thanks for the help

[Henrik Böving]

I'm not quite sure what you are asking for but if you have some element x of typeSubtypeyou can get the value with x.val and if you want to construct one you can use the Subtype.mk constructor

[Mathias Schack Rabing]

Thank you it was the Subtype.mk contructor i couldn't find

[Kevin Buzzard]

You can use pointy brackets \<n, proof\> as well