Finset.filter_congr_decidable

Stream: mathlib4

[Yaël Dillies]

docs3#finset.filter_congr_decidable was optimistically no-aligned with the following message:

-- Porting note: likely no longer relevant with `Bool`s

Let me just tell you that this is wrong, since I'm currently fixing some regressions in #7021.

[Eric Wieser]

This is because filter at one point took its predicate as a bool

[Yaël Dillies]

How was that supposed to fix anything?

[Eric Wieser]

When the filtering was by bool, there was no decidable argument, which is why the lemma was removed

[Eric Wieser]

Then we changed it back but forgot to re-add the lemma

[Yaël Dillies]

Hmm... okay