Commit 2026-03-21 13:13 ae57752b

fix(Tactic/Linarith): don't throw an error for ¬a ≤ b hypotheses (#36782) This PR fixes a bug in linarith that causes the tactic to error if there is a hypothesis ¬a ≤ b where the order is not a linear order. In doing this fix, I decided to merged the preprocessors removeNegations and filterComparisons, which I think makes the code more understandable.