simp_rw [bij_fun] at heq
case left
a b : ℝ
heq : bij_fun a = bij_fun b
⊢ a = b
case left
a b : ℝ
heq :
  { val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } =
    { val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) }
⊢ a = b