refactor(order/filter): move some proofs to `bases` (#3478)
Move some proofs to `order/filter/bases` and add `filter.has_basis` versions.
Non-bc API changes:
* `filter.inf_ne_bot_iff`; change `∀ {U V}, U ∈ f → V ∈ g → ...` to `∀ ⦃U⦄, U ∈ f → ∀ ⦃V⦄, V ∈ g → ...`
so that `simp` lemmas about `∀ U ∈ f` can further simplify the result;
* `filter.inf_eq_bot_iff`: similarly, change `∃ U V, ...` to `∃ (U ∈ f) (V ∈ g), ...`
* `cluster_pt_iff`: similarly, change `∀ {U V : set α}, U ∈ 𝓝 x → V ∈ F → ...` to
`∀ ⦃U : set α⦄ (hU : U ∈ 𝓝 x) ⦃V⦄ (hV : V ∈ F), ...`
