How can I be faster at wlog

Stream: general

[(deleted)]

import Mathlib
theorem extracted_1 (m n p q : ℕ) (hm : 0 < m) (hn : 0 < n) (hp : 0 < p) (hq : 0 < q)
  (h : m * n * p * q = 6 * (m - 1) * (n - 1) * (p - 1) * (q - 1)) (hm_ne_one : m ≠ 1) (hn_ne_one : n ≠ 1)
  (hp_ne_one : p ≠ 1) (hq_ne_one : q ≠ 1) (hNotAllGe3 : ¬(3 ≤ m ∧ 3 ≤ n ∧ 3 ≤ p ∧ 3 ≤ q)) :
  ({m, n, p, q} : Multiset ℕ) = {9, 4, 2, 2} ∨ ({m, n, p, q} : Multiset ℕ) = {6, 5, 2, 2} ∨ ({m, n, p, q} : Multiset ℕ) = {4, 3, 3, 2} := sorry

To prove this theorem, the easiest approach is to do a WLOG to assume m >= n and n >= p and p >= q. To impose this order I use the wlog tactic with List.mergeSort, then use List.Perm.prod_eq and List.Perm.foldl_op_eq. However this is laborious. Is there a faster way?

[(deleted)]

After wlog the theorem becomes solvable with AI. I'm just asking about how I can do the wlog more quickly

[Yan Yablonovskiy 🇺🇦]

Huỳnh Trần Khanh said:

After wlog the theorem becomes solvable with AI. I'm just asking about how I can do the wlog more quickly

which AI

[(deleted)]

Cursor with GPT-5, setup is in #lean4 > Vibe Proving