Simplifying lambda expressions

Stream: new members

[Rick Koenders]

Is there a way (in tactic mode) to simplify lambda expressions that are applied to an element? So a way to transform (λ n : ℕ, foo n) x into foo x. So far I have found that simp will do this, but squeeze_simp does not say what lemma is used to simplify this expression (probably because they are definitionally equal). In my code I'd like to use this at this point (irrelevant context removed):

import tactic

example (a : ℕ → ℕ) (h : ∀ x : ℕ, ¬(λ (n : ℕ), a n ≠ 0) x) : ∀ n : ℕ, a n = 0 :=
begin
    simp only [not_not, ne.def] at h, -- Found this using squeeze_simp
    exact h,
end

Note that using tactics like rw ne.def at h and rw not_not at h do not work: Lean does "not find instance of the pattern in the target expression".
Can you prove this without using simp? If it is possible, is using simp here preferred over that alternative?

[Reid Barton]

The usual recommendation is dsimp only [] at h

[Patrick Massot]

You can even omit the empty list.

[Rick Koenders]

Just found out that the reason rw not_not at h doesn't work is because of the ∀, not because of the λ. The following is a valid proof without simp:

example (a : ℕ → ℕ) (h : ∀ x : ℕ, ¬(λ (n : ℕ), a n ≠ 0) x) : ∀ n : ℕ, a n = 0 :=
begin
    intro n,
    have hn := h n,
    rw not_not at hn,
    exact hn,
end

Thanks for the suggestions everyone.