wlog

[jcommelin]

It is nontrivial (currently for me impossible) to use wlog in the following example.

lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) :
  (1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 :=
begin
  wlog : a ≤ b ∧ b ≤ c, -- or some similar incantation involving "using ..."
end

I am perfectly happy with having to prove some side goals.

[kckennylau]

Per https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/wlog.20is.20slow/near/195434556:

import tactic.wlog data.rat.order

lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) :
  (1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 :=
begin
  wlog : a ≤ b ∧ b ≤ c using [a b c, a c b, b a c, b c a, c a b, c b a] tactic.skip,
end

[jcommelin]

using [a b c, a c b, b a c, b c a, c a b, c b a] tactic.skip can we shorten this to using (perms_of [a,b,c])?

[cipher1024]

@jcommelin I like your suggested syntax. My only worry is that, because the number of cases is n! for n variables, it's easy to make it unreasonably slow or otherwise expensive. What do you think of setting an upper limit of 4 or 5 variables with an error message if you go over but with the option to override it?

[jcommelin]

Yup, that seems totally reasonable. I think that the typical use case will be n = 3, sometimes n = 4. (And with n = 2 the new syntax doesn't save bytes.)