Subgoal for each argument of a function

Stream: new members

[Calvin Lee]

Hi!
I'm trying to prove a goal r when I have a function f : p → q → r
is there any clever tactic to create subgoals for p and q instead of just doing something like

have pf₁ : p, { ... },
have pf₂ : q, { ... },
exact f pf₁ pf₂

[Roberto Alvarez]

You can do refine f _ _ or simply apply f