fix: use match with Decidable in List instances

[collares]

This works around leanprover/lean4#2552; the idea is copied from leanprover-community/mathlib4#7232. Fixes the timeouts described in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/brute.20force.20calculation.20of.20Bell.2FStirling.20numbers.

[kbuzzard]

Of course the correct question is "why is this happening" :-) If that could be isolated and fixed, this PR wouldn't be needed!

[collares]

True! In the meantime, the forall/exists instances in Logic.lean and Data/Option/Basic.lean probably should have the same workaround applied to them too.

[collares]

(A previous stupid comment of mine was deleted)

[kim-em]

This is worse than the issue described in leanprover/lean4#2552: here it's not cases that is a problem, but merely if.

Would you be able to open a lean4 issue demonstrating this problem?

Hacky workarounds like these need to be accompanied by links in the source code to the relevant issues, so we can undo them later.

[collares]

Thanks for not blindly merging. Turns out I hadn't fully reverted some other changes, and this PR is not helpful for fixing the Zulip issues. Closing.