misleading error message about linarith

[jnarboux]

Sometimes On conclut par .... displays
linarith failed to find a contradiction, where as the goal as nothing to do with linear arithmetic,I understand that the tactic tries different things, but failures should not be displayed, I think.

[mmasdeu]

Here is an example of such behavior. More annoyingly, the help tactic suggests to use "On conclute par..." in this case.

example (n : ℕ) (h : n ∉ Finset.range n) : n ∉ Finset.range n := by
  We conclude by h