Unfolding let definition

Stream: new members

[Roberto Pettinau]

Hi everyone! Is it possible to unfold a let definition in Lean4? Here is a simple example:

def test (n: Nat): 0 = 1 :=
  let zero: Nat := 0
  let one: Nat := 1
  by
    have h1: 0 = zero := by rfl;
    rw [h1]
    have h2: 1 = one := by rfl;
    rw [h2]

I would like to somehow be able to change my current goal from zero = one to 0=one, by doing some kind of unfold zero.

I am aware of the existence of dsimp, but that would transform the goal into 0=1

[Kevin Buzzard]

What about dsimp only [zero] or if that doesn't work, I can't quite remember the syntax but something like dsimp (config := {zeta := false}) only [zero]?