Proving a symmetric iff with symmetric hypotheses

Stream: new members

[Joanna Choules]

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?)

[Floris van Doorn]

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.

[Joanna Choules]

That seems a good plan, thanks!