apply bug with `fun a => _`

Stream: mathlib4

[Jireh Loreaux]

I'm not sure if this is a problem with apply exactly, but I've noticed during porting several times that with something of the form apply ... fun a => _ the a is actually not introduced into the context, which results in an error. Generally, switching to refine (or refine') solves the problem. Is this a bug in apply, or is this expected behavior? If the latter, should mathport be changed? @Mario Carneiro :up: since you want us to report mathport problems.

[Ruben Van de Velde]

I've noticed the same issue with rw [foo fun a => _]

[Floris van Doorn]

I think it works if you replace the _ by ?_

[Yury G. Kudryashov]

I was replacing applys with refines.