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.
see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20and.20ENNReal and the mwe of @eric-wieser there:
Seems like
linarithshould ignore (in)equalities in the context it doesn't get.