linarith not ignoring irrelevant (in)equalities

[mo271]

see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20and.20ENNReal and the mwe of @eric-wieser there:

import Mathlib.Tactic.Linarith

example : 0 ≤ 1 := by linarith -- ok

example (s : Set ℕ) (h : s = ∅) : 0 ≤ 1 :=
by linarith
/-
failed to synthesize
  AddGroup (Set ℕ)
-/

Seems like linarith should ignore (in)equalities in the context it doesn't get.

[dwrensha]

I ran into this problem recently too: https://github.com/dwrensha/math-puzzles-in-lean4/blob/f79693080e1a43c3d9f82098ebfd26c28abadaed/MathPuzzles/Usa1998Q5.lean#L74

[mo271]

I see, you used the same workaround: clear the interfering lemmas before invoking linarith.