simp doesn't work without placeholders

Stream: mathlib4

[Eric Wieser]

I'm seeing some very weird behavior in !4#2899; simp only [Set.mem_vsub (β := _), ...] makes progress on a goal that simp only [Set.mem_vsub, ...] does not. Why does filling an implicit argument to docs4#Set.mem_vsub with a placeholder change the behavior?

[Eric Wieser]

The file is also full of places where simp [lineMap_apply _] succeeds but simp [lineMap_apply] would fail

[Eric Wieser]

At a guess, this is something to do with outParam handling in simp

[Floris van Doorn]

My guess is that it depends on whether a name or an expression is passed to simp. What does simp only [(Set.mem_vsub), ...] do?

[Eric Wieser]

That works!

[Eric Wieser]

In fact, that now consistently fixes the problems in the file

[Kevin Buzzard]

That's a really nice hack to know, but is it really what we want?

[Eric Wieser]

I think simp [foo _] is a worse hack than simp [(foo)]; the latter at least raises red flags that something weird is going on

[Eric Wieser]

Am I right in thinking that simp [foo] really means simp [(@foo)]?