simp only [add_sub_cancel, Real.log_exp] at heq
case left
a b : ℝ
heq :
  Real.log
      (↑{ val := Real.exp a + Real.sqrt 2, property := (_ : Real.exp a + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2) =
    Real.log
      (↑{ val := Real.exp b + Real.sqrt 2, property := (_ : Real.exp b + Real.sqrt 2 > Real.sqrt 2) } - Real.sqrt 2)
⊢ a = b
case left
a b : ℝ
heq : a = b
⊢ a = b