adding hypothesis from lemma

Stream: new members

[Peter Nelson]

If I am in tactic mode and there is a lemma (foo a b ) elsewhere, is there a way to add (foo a b) directly to my hypotheses without using 'have' and retyping the full statement of foo?

[Reid Barton]

have h := foo a b, or have := foo a b. You don't have to give the type if you don't want to.

[Peter Nelson]

Thank you!