# Zulip Chat Archive

## 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