rw unfolds lets

Stream: lean4

[Eric Wieser]

Is this change in 4.12.0 expected?

def foo (x : Nat) : Nat := let three := x + 2; three

example : foo x = 2 + x := by
  rw [foo]
  -- in 4.11.0 the `let` is still present, in 4.12.0 it has been inlined