rewriting `(λ x, expr) x`

Stream: new members

[Jason Orendorff]

I almost never actually want (λ x, expr) x in a goal, but what's the best way to get rid of it? I noticed simp only [] does the trick, but maybe that is fragile.

[Rob Lewis]

simp only is fine, dsimp only is fine too. If you're unexpectedly finding this pattern in your goals a lot, maybe try to investigate what's causing it, it's not expected that things randomly get expanded like that.

[Jason Orendorff]

Thanks. It happens when there's a definition like tendsto that takes a function, when tendsto gets unfolded.