## Stream: new members

### Topic: adding hypothesis from lemma

#### Peter Nelson (Aug 14 2020 at 18:02):

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 (Aug 14 2020 at 18:05):

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 (Aug 14 2020 at 18:07):

Thank you!

Last updated: May 10 2021 at 19:16 UTC