Commit 2026-09-03 14:21 bb5364cb

fix: remove DecidableEq Prop instance (#42369) Convert the LinearOrder Prop and CompleteLinearOrder Prop instances into defs, to avoid providing a global DecidableEq Prop instance. We can convert them back when the decidability fields are removed from LinearOrder, but very few places need LinearOrder Prop so this seems like a good fix until that happens. Note that the DecidableEq Prop instance causes diamonds with instDecidableEqOfIff. See [#mathlib4 > leaked `DecidableEq Prop`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/leaked.20.60DecidableEq.20Prop.60/with/564769361)