WLOG trick

Stream: new members

[Suryansh Shrivastava]

Is there a lean4 counterpart to the statement that if $a \neq b$, we can assume $a < b$. Here $a,b: \N$

[Chris Bailey]

What if a > b? If you meant a < b ∨ a > b, it appears to be in mathlib as lt_or_gt_of_ne

[Anatole Dedecker]

I think Suryansh meant that if the hypotheses and the goal are symmetrical in a and b, then you can treat only the a < b case. We have tactic#wlog to do that, but to be fair I’ve never used it. The manual solution is to start by proving your result for all a' and b' which satisfy ˋa' < b'ˋ, and then apply this to either ˋ(a, b) or ˋ(b, a) depending on the case

[Jireh Loreaux]

Anatole meant tactic#wlog

[Yakov Pechersky]

There is also the much less powerful, but conceptually simpler tactic#swap_var

[Kevin Buzzard]

Before WLOG I used to do this manually. You write down the appropriate statement of the from a<=b + symmetric hypotheses -> symmetric result and then apply it twice