drop hypothesis from local context

Stream: general

[Johan Commelin]

Please remind me, which tactic removes hypotheses from the local context? Because I have used up some hyptheses, and I won't use them again, but the proof state is filling an entire screen.

[Johan Commelin]

I couldn't find the tactic in TPIL...

[Sean Leather]

clear

[Johan Commelin]

aah, thanks

[Sean Leather]

For reference: https://leanprover.github.io/reference/search.html?q=clear&check_keywords=yes&area=default

[Johan Commelin]

I see it is in TPIL, but the words "drop" or "remove" are not in its description

[Sean Leather]

You could try browsing this section if you're looking for something similar in the future.

[Mario Carneiro]

You can also use replace in place of have to clear old hyps as well

[Sean Leather]

I didn't know about replace.