rw はローカル変数の展開は行わない

[Seasawher]

def smallNat : {x : Nat // x < 5 } := by
  let n := 2
  have h : n < 5 := by
    -- rw はローカル変数の展開は行わない
    fail_if_success rw [n]

    -- dsimp で展開できる
    dsimp [n]

    -- あとは 2 < 5 を示せばよいだけ
    show 2 < 5
    decide

  exact ⟨n, h⟩