Stream: new members
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
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
Joanna Choules (Mar 05 2021 at 18:48):
That seems a good plan, thanks!
Last updated: May 13 2021 at 18:26 UTC