Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-21 22:33 d17db717

View on Github →

chore(*): golf proofs about filter.Coprod (#10400) Also add some supporting lemmas.

Estimated changes