Zulip Chat Archive

Stream: new members

Topic: duplicate a hypothesis


view this post on Zulip Michael Beeson (Sep 03 2020 at 04:59):

Suppose I have a hypothesis h. I need to do something to that hypothesis now, using cases.
But later I need to use hypothesis h. Using cases will "clear" h so it's not available later.
Therefore I need to make a copy of h before I use cases on it. How can I do that? (in tactic mode).

view this post on Zulip Alex J. Best (Sep 03 2020 at 05:00):

have h' := h should work

view this post on Zulip Michael Beeson (Sep 03 2020 at 05:00):

Thank you!

view this post on Zulip Alex J. Best (Sep 03 2020 at 05:01):

You could also restructure the proof so that the cases h is within a { } block, by using suffices or have for your intermediate goals, outside the { } the original h will be left intact


Last updated: May 14 2021 at 06:16 UTC