## Stream: new members

### Topic: Simplifying lambda expressions

#### Rick Koenders (Jun 05 2020 at 15:17):

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 (Jun 05 2020 at 15:18):

The usual recommendation is dsimp only [] at h

#### Patrick Massot (Jun 05 2020 at 15:30):

You can even omit the empty list.

#### Rick Koenders (Jun 05 2020 at 15:33):

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.

Last updated: May 14 2021 at 07:19 UTC