forgetting assumptions in goal

Stream: new members

[Chris M]

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]

@Chris M clear

[Chris M]

Great!