How to avoid (by rfl : ... = ...) after "let"

Stream: lean4

[Mitchell Lee]

Sometimes, I want to use let to give a name to an expression that appears, potentially multiple times, in a goal or hypothesis. For example:

import Mathlib

example (x : ℝ) : Real.sin (Real.exp (x ^ 3) - x) = Real.sin (Real.exp (x ^ 3) - x) + 0 := by
  let y := Real.sin (Real.exp (x ^ 3) - x)
  sorry

Now, suppose that I want to rewrite the goal using the variable y instead of x. The easiest way I know to do this is rw [(by rfl : Real.sin (Real.exp (x ^ 3) - x) = y)] or rw [← (by rfl : y = Real.sin (Real.exp (x ^ 3) - x))]. Is there any easier way to do it?

[Matt Diamond]

instead of let, use set

[Mitchell Lee]

Thanks!