fun in goal

Stream: new members

[Alice]

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]

The usual way is dsimp only

[Alice]

Thanks you