apply incompatibility

Stream: mathlib4

[Yury G. Kudryashov]

In Mathlib 3, apply f (λ x, _) worked as refine f (λ x, _). In Mathlib 4, it works as refine' f _. I fix it by using refine instead of apply.

[Floris van Doorn]

see also this thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/apply.20doesn't.20like.20.60fun.20x.20.3D.3E.20_.60

[Mario Carneiro]

The fact that fun x => _ acts like _ in apply seems like a lean bug that should be reported

[Mario Carneiro]

refine' does not exhibit the same behavior (I think that was an earlier bug report)