Replace metavariables by appropriate quantifiers

Stream: Is there code for X?

[Frédéric Le Roux]

When Lean provides a property with some metavariables, is there a simple automatic way to replace the property by a quantified version with no metavariables?

Here is a concrete example. I have the definition of the image of a set,

lemma theorem.direct_image {f:X → Y} {x : X} {A : set X} :
x ∈ A → f x ∈ f '' A

and I want to apply this the followaing way:

example (y:X) (B : set X) (g: X → Y) (H1: y ∈ B) : true :=
begin
    have H2 :=  theorem.direct_image H1,
end

Lean can infer x and A, but not f, so we get

H2 : ?m_2 y ∈ (?m_2 '' B)

with some metavariable. I would love to get

H2bis : ∀ f: X→Y, f y ∈ (f '' B).

Is there an automatic way to go from H2 to H2bis (or to get directly H2bis)?

[Scott Morrison]

Often this is a sign that you are over using implicit arguments, and you should have just made f an explicit argument in the first place, so that it was possible to specify it here

[Scott Morrison]

While opinions vary, mathlib probably suffers a lot from this.

[Scott Morrison]

You can use @ at the call site to make all arguments explicit.

[Scott Morrison]

But this is slightly stinky.