wlog timeouts

Stream: general

[Mantas Baksys]

While solving an inequality, I would be interested in using the wlog tactic to only have to work under a specific assumption. For example, given the inequality to prove 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a), I would like to assume that a ≤ b ∧ b ≤ c. I tried using wlog h : a ≤ b ∧ b ≤ c using [a b c, b c a, c a b, a c b, c b a, b a c] but it keeps timing out on my machine. Is there a way to fix this while still using wlog? What would be the alternatives of wlog? Here's an MWE (the inequality itself is not provable without extra assumptions, which I didn't care to include). Thanks!

import data.real.basic

theorem inequality (a b c : ℝ) : 0 ≤ a ^ 2 * b * (a - b) + b ^ 2 * c * (b - c) + c ^ 2 * a * (c - a) :=
begin
  wlog h : a ≤ b ∧ b ≤ c using [a b c, b c a, c a b, a c b, c b a, b a c] -- timeouts
end

[Eric Rodriguez]

some discussion on this:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Odd.20residues.20mod.208/near/272740760

[Eric Rodriguez]

hopefully it speeds up in lean4, I'd like wlog too :(

[Mantas Baksys]

I don't think swap_var suffices for my use case. So I guess there's no other better way apart from just a case bash?

[Eric Rodriguez]

you can maybe do a two-term wlog and then swap_var with some le_or_le stuff, but otherwise yes :/ it's very sad

[Reid Barton]

Sorry if I am missing something obvious but isn't this inequality only cyclically symmetric? How are you getting to $a \le b \le c$?

[Yaël Dillies]

It is once you expand terms out.

[Reid Barton]

I see $a^3 b + b^3 c + c^3 a +$ (symmetric stuff)

[Yaël Dillies]

Oh wait, right.