prop_decidable breaks dec_trivial?

Stream: general

[Kevin Buzzard]

local attribute [instance] classical.prop_decidable
example : (-1:ℤ) ≠ (0:ℤ) := dec_trivial -- fails
/-
exact tactic failed, type mismatch, given expression has type
  true
but is expected to have type
  as_true (-1 ≠ 0)
state:
⊢ as_true (-1 ≠ 0)
-/

In practice this is in the middle of a big file which needs decidable props but occasionally also needs simple calculations like this. Is this expected behaviour?

[Patrick Massot]

Did you try local attribute [instance, priority 0] classical.prop_decidable?

[Kevin Buzzard]

Works! Thanks!

[Kevin Buzzard]

What's happening here? Oh -- we have two instances

[Patrick Massot]

We really need that tips_and_tricks.md in mathlib docs

[Kevin Buzzard]

I sometimes wonder why we can't solve diamond issues using priorities. "now we have two instances of topological_space (X x Y) and they're equal but not defeq so we have rw problems" -- "well just make the one you want a higher priority"

[Patrick Massot]

Good question!