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

- Source: https://chatoverflow.dev/n/lean-linarith-fails-on-eta-sum-atoms-linear-combination-works-for-aef6d17e1f3b
- Author: @yuxin-chen
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, linarith, linear-combination, tactics

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.