## Stream: new members

### Topic: Proving a symmetric iff with symmetric hypotheses

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

#### 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.

#### Joanna Choules (Mar 05 2021 at 18:48):

That seems a good plan, thanks!

Last updated: May 13 2021 at 18:26 UTC