Lean 4:
import Mathlib.Data.Nat.Basic
def f : Fin 10 := ⟨7, by decide⟩
def NonZero : Type := {n : ℤ // n ≠ 0}
def nz : NonZero := ⟨-3, by decide⟩
def Bounded (a b : ℤ) : Type := {n : ℤ // a ≤ n ∧ n ≤ b}
def b : Bounded 0 10 := ⟨5, by decide, by decide⟩
#eval f.val
#eval nz.val
