mathlib3

a095eaeb - feat(order/filter/*): `filter.pi` is countably generated (#15632)

feat(order/filter/*): `filter.pi` is countably generated (#15632) * rename `filter.has_basis_infi` to `filter.has_basis_infi'`, add new `filter.has_basis_infi`; * move `prod.is_countably_generated`, golf, add `coprod.is_countably_generated`; * `is_countably_generated_seq` is no longer an instance, `infi.is_countably_generated` is better; * add `infi.is_countably_generated` and `pi.is_countably_generated`; * prove `prod.fist_countable_topology` (from the sphere eversion project) and `pi.first_countable_topology`; * generalize `pi.second_countable_topology` from `encodable` to `countable` so that it automatically applies to finite types.