## Stream: new members

### Topic: WLOG trick

#### Suryansh Shrivastava (May 24 2023 at 17:54):

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

#### Chris Bailey (May 24 2023 at 18:46):

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 (May 24 2023 at 19:11):

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 (May 24 2023 at 19:19):

Anatole meant tactic#wlog

#### Yakov Pechersky (May 24 2023 at 19:39):

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

#### Kevin Buzzard (May 24 2023 at 19:45):

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

Last updated: Dec 20 2023 at 11:08 UTC