I'm not sure this comes up organically, but in testing I found that a Goal of type ... /\ False, results in the following message after using "We show both directions."
Add the following line to the proof:
We need to show that (Derive a contradiction.).
or write:
We conclude that (Derive a contradiction.).
if no intermediary proof steps are required.
The proper thing here should probably be: "We need to derive a contradiction" or "Contradiction." (Replacing "Derive a contradiction" by False" would be a reasonable fallback.
I'm not sure this comes up organically, but in testing I found that a Goal of type ... /\ False, results in the following message after using "We show both directions."
Add the following line to the proof:
We need to show that (Derive a contradiction.).
or write:
We conclude that (Derive a contradiction.).
if no intermediary proof steps are required.
The proper thing here should probably be: "We need to derive a contradiction" or "Contradiction." (Replacing "Derive a contradiction" by False" would be a reasonable fallback.