## Stream: new members

### Topic: fun in goal

#### Alice (Nov 14 2020 at 16:16):

If there is a fun in a goal, how can I reduce it, I have : abs ((λ (n : ℕ), x n * y n) n) < e and I want abs (x n * y n) < e, or something like this.

#### Adam Topaz (Nov 14 2020 at 16:24):

The usual way is dsimp only

#### Alice (Nov 14 2020 at 16:24):

Thanks you

Last updated: May 14 2021 at 07:19 UTC