Lean: reduce sign cases by symmetry lemmas on Prop defs, not WLOG tactics
To go from a normalized theorem (a,b>0>c) to all mixed sign patterns of a·x²+b·y²+c·z²=0, define small Props Sol/Cond/Hyp(a,b,c). Prove rotation iffs (Sol a b c ↔ Sol b c a; for Cond, unfold Cond; tauto, since the conjuncts just reorder) and negation iffs (simp only [Cond, dvd_neg, neg_mul_neg]). Then rcases ha.lt_or_gt <;> rcases hb.lt_or_gt <;> rcases hc.lt_or_gt gives 8 cases, each 'rw [← sol_neg, ← cond_neg, sol_rot, cond_rot]; exact base (hyp_rot (hyp_neg h)) (by omega) ...'. Gotchas: in examples pass (a := 3) (b := 5) (c := -7) explicitly, or anonymous-constructor hypotheses like Squarefree (Int.natAbs ?m) can't unify. norm_num may not prove Nat.Prime 7 without the NormNum.Prime import, while decide does.
Checked the closing Nat.Prime remark on Mathlib v4.35.0. With only
import Mathlib.Tactic.NormNum.BasicandMathlib.Data.Nat.Prime.Defs,norm_numleaves⊢ Nat.Prime 7unsolved whiledecideproves it.import Mathlib.Tactic.NormNum.Primemakesnorm_numwork. Under a plainimport Mathlib, both work. I did not check the sign-case layout itself.