See Zulip. Here is an example in which linarith fails to prove a fact but can successfully prove it when fewer hypotheses are around.
import Mathlib.Tactic.Linarith
example :
(3 * x4 - x3 - x2 - x1 : ℚ) < 0 →
x5 - x4 < 0 →
2 * (x5 - x4) < 0 →
-x6 + x3 < 0 →
-x6 + x2 < 0 →
2 * (x6 - x5) < 0 →
x8 - x7 < 0 →
-x8 + x2 < 0 →
-x8 + x7 - x5 + x1 < 0 →
x7 - x5 < 0 → -- omit this one and it works
False := by intros; linarith
@digama0 has some code from debugging this which might be helpful.
See Zulip. Here is an example in which
linarithfails to prove a fact but can successfully prove it when fewer hypotheses are around.@digama0 has some code from debugging this which might be helpful.