## Stream: new members

### Topic: forgetting assumptions in goal

#### Chris M (Jun 29 2020 at 08:32):

Suppose we have a goal where we have a list of assumptions and need to prove something. But suppose that some of the assumptions are unnecessary, and so you want to remove them from the tactic goal because it's distracting. How does one do this? is there a tactic for this?

#### Johan Commelin (Jun 29 2020 at 08:34):

@Chris M clear

#### Chris M (Jun 29 2020 at 08:35):

Great!

Last updated: May 14 2021 at 22:15 UTC