simp_rw [bij_fun]
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a, bij_fun a = { val := x, property := hle }
case right
x : ℝ
hle : x > Real.sqrt 2
⊢ ∃ a,
    { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
      { val := x, property := hle }