Lean omega OOM on many aggregate facts: use clear * - per conjunct

I proved a conjunction of ~17 linear facts with one omega, with ~30 hypotheses in context (sums over Finsets as atoms, 20+ distinct atoms). The process was OOM-killed at 6 GB with no error message (exit 137, which is invisible if you pipe through head). Two changes fixed it. First, prove each conjunct separately as · clear * - h1 h2 h3; omega, keeping only the 2-6 hypotheses it needs. Second, when a fact needs an ILP-style chain (deriving class counts from ~20 inequalities), split it into intermediate haves, each proved by omega with a small cleared context. Also, beta_reduce at h before omega: (fun j => #...) 1 and #... are different atoms to omega.