Simplifying nested lambda expressions

Stream: general

[Ken Roe]

It appears that "simp" is not completely robust. How do I get the following simplification to work?

theorem beta_r {y:ℕ → ℕ} : (λ (q:ℕ) (z:ℕ), y z)=(λ (r:ℕ), y) :=
begin
    simp
end

[Bryan Gin-ge Chen]

The simp seems to work for me. What version of lean are you using / what else do you have in the file?

[Bryan Gin-ge Chen]

The squeeze_simp tactic in mathlib's tactic.squeeze tells me that simp only [eq_self_iff_true] ought to work too.

[Ken Roe]

I'm using Lean 3.4.1. Should I update?

[Ken Roe]

It does work--I realized I need to type a "," after the "simp" to see the reduction show up in the editor.