Canonical example for wlog tactic

Stream: new members

[Dan Abramov]

I've looked at the wlog documentation and I vaguely understand the purpose (exploiting symmetry to avoid repeating an argument twice), and even some of the mechanics (prove it for one side, then prove... that something something with inverted something).

But the full mechanics elude me (what exactly are we proving in how the two cases relate? what exactly does the inverted context in this give us?)

I would very much appreciate a brief description of why wlog "works" (i.e. what it does logically), or a tiny 5-liner motivating example showing what kind of things it lets us prove (and how to wield this context in a useful way there).

Thanks!

[Dan Abramov]

If it helps to be more concrete, I'm reading through this proof and I don't have any idea of what's going on inside that wlog. So I'm hoping to get enough understanding to follow those lines and nod along. I had no difficulty proving this lemma on my own, but I did not use wlog and it ended up more cumbersome.

[Riccardo Brasca]

Unfortunately, working with wlog is often a pain. The mathematical idea is that if you have a statement about two real numbers a and b, that is symmetric in those variables, you can always assume a ≤ b. The reason is that the same proof will work just exchanging a with b in the case b ≤ a.

On the other hand wlog asks you to prove that the case when a ≤ b holds implies the case when a ≤ b does not hold. This is similar, but not the same, to the usual reasoning "let's assume a ≤ b since clearly the same proof will work in the case b ≤ a.

[Dan Abramov]

Yea at this point I'm just trying to understand what Lean's wlog actually does (aside from the mathematical wlog it aspires to) and why in some subset of cases it seems to at least partially cover the same need.

On the other hand wlog asks you to prove that the case when a ≤ b holds implies the case when a ≤ b does not hold.

Ok I can follow this one — but what's the deal with this context. What is that implication chain composed of and what is the intuition behind it? And how do I usually use it?

[Riccardo Brasca]

In your example you have two real numbers s r : ℝ such that h : s ≠ t, a sequence a : ℕ → ℝ such that hs : TendsTo a s and hr : TendsTo a r. You have to prove False.

wlog h2 : s < t leaves you with two goals: the second one is what you want (same goal as before, with the new assumption s < t). Let's have a look at the first one. The goal is still False, you have the same hypotheses, but moreover you have that

this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t

h2 is clear, it is the negation of s < t. The this assumption is the fact that the theorem is true in the case s < t (note that all the things before → s < t are the context of your original statement). In practice this first goals means "suppose you are able to prove the theorem assuming moreover s < t (and let's call this the fact that you can prove the theorem in this case), then prove the theorem in the other case, ie when ¬s < t".

[Riccardo Brasca]

I am afraid that the usual answer to "how to use wlog?" is "don't use wlog if it's not working immediately"