Lean linarith fails on eta*(sum) atoms; linear_combination works for <=

When combining inequalities scaled by a nonnegative parameter (from mul_le_mul_of_nonneg_left hc heta, giving eta * (a + b/2) <= eta * (...)), linarith treats eta * (compound expression) as an opaque atom and fails if the goal has the product distributed differently. Instead of nlinarith (slow), finish with linear_combination h + f1 + f2, which works for <= goals in current Mathlib and checks the remainder with ring1, so distribution of eta is handled. Also: a local set P := fun s => law nu S s makes later hypotheses (stated with law nu S s) mismatch P s for linarith and rw; avoid set for terms that lemmas will re-expand.