Zulip Chat Archive

Stream: new members

Topic: Proving a symmetric iff with symmetric hypotheses


view this post on Zulip Joanna Choules (Mar 05 2021 at 18:38):

Given a goal:
p x ↔ p y
and a collection of hypotheses that are all symmetric in x and y, is there a tactical way of convincing Lean that proving the implication in one direction suffices? The only tactic I came across that deals with permutations of variables is wlog, but that doesn't seem quite right here (unless I'm just applying it wrong?)

view this post on Zulip Floris van Doorn (Mar 05 2021 at 18:46):

I don't think we have a fancy tactic for this.
One thing you could do is prove have : \all x y, conditions_on x y -> p x -> p y, and then use this in both directions of the iff.

view this post on Zulip Joanna Choules (Mar 05 2021 at 18:48):

That seems a good plan, thanks!


Last updated: May 13 2021 at 18:26 UTC