make an argument implicit

Stream: Is there code for X?

[Felix Weilacher]

Let's say I have a hypothesis h : ∀ x : α, p x. Is there a quick way to replace this with h : ∀ {x : α}, p x?

A not quick way is to just introduce this new version with have and prove it using the old version, but I'd like to avoid typing out p again in cases where it's complicated.

[Riccardo Brasca]

Not exactly an answer, but if the problem is that x is a very long expression that can be inferred you can write h _ and Lean will do the magic.

[Felix Weilacher]

yeah, this is what I've been doing. My reason for wanting to avoid it is that I actually have many arguments, so it becomes h _ _ _ _ etc. Still maybe it is the best solution.

[Kevin Buzzard]

change ∀ {x : α}, _ at h,

[Felix Weilacher]

That works well, thanks!