CardinalInterFilter vs CountableInterFilter: refactor?

Stream: mathlib4

[Josha Dekker]

Recently I've added docs#CardinalInterFilter as a typeclass to mathlib. This definition generalizes docs#CountableInterFilter and the file contains a proof that they are in fact the same for a specific cardinal.

@Oliver Nash and I thought that we could consider refactoring the proofs in docs#CountableInterFilter in terms of docs#CardinalInterFilter. The main trade-off would be a shorter file for docs#CountableInterFilter (less defs, less API) versus the fact that this would then need to transitively import Mathlib.SetTheory.Cardinal.Cofinality.

I'm curious what you think, I'm more than happy to carry out the refactor! Note that all results in docs#CountableInterFilter generalized to docs#CardinalInterFilter: the first half of the results has already landed in mathlib, the other half is in #11578.

Option 1: don't refactor
Option 2: refactor
Option 3: Refactor, but split CardinalInterFilter into a file with more basic results (which then only needs to import Mathlib.SetTheory.Cardinal.Ordinal`) and a file with the other results (which then imports Mathlib.SetTheory.Cardinal.Cofinality). As such, CountableInterFilter should only transitively need Mathlib.SetTheory.Cardinal.Ordinal instead of Mathlib.SetTheory.Cardinal.Cofinality.

[Josha Dekker]

/poll What to do
Don't refactor
Refactor
Split and refactor

[Johan Commelin]

cc @Yury G. Kudryashov who wrote the original

[Yury G. Kudryashov]

I'm a bit worried about adding more dependencies, otherwise I don't care (both refactor and don't refactor LGTM)

[Oliver Nash]

OK let's live with the duplication, at least for now.