use (Real.log (x - Real.sqrt 2))
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 }
case h
x : ℝ
hle : x > Real.sqrt 2
⊢ { val := Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2,
      property := (_ : Real.exp (Real.log (x - Real.sqrt 2)) + Real.sqrt 2 > Real.sqrt 2) } =
    { val := x, property := hle }