simp not idempotent with `let`

Stream: general

[Eric Rodriguez]

Hey all! I've been trying to use a lot of lets in my code for clarity, but it feels like it always ends up being a pain to do so. For example, look at this mwe:

example : true :=
begin
  let some_fun := λ asda : ℕ, ite (asda = 23 ∨ asda = 420) 123 456,
  suffices : some_fun 23 = some_fun 420, by trivial,
  simp [some_fun], simp,
end

For some reason, I need both simps; if I try just one, it pretty much just unfolds some_fun and then gives up. Is this something one of the hidden simp parameters can solve?