feat(order/filter): change definition of inf (#8657)
The current definition of `filter.inf` came directly from the Galois insertion: `u ∈ f ⊓ g` if it contains `s ∩ t` for some `s ∈ f` and `t ∈ g`, but the new one is tidier: `u ∈ f ⊓ g` if `u = s ∩ t` for some `s ∈ f` and `t ∈ g`. This gives a stronger assertion to work with when assuming a set belongs to a filter inf. On the other hand it makes it harder to prove such a statement so we keep the old version as a lemma `filter.mem_inf_of_inter : ∀ {f g : filter α} {s t u : set α}, s ∈ f → t ∈ g → s ∩ t ⊆ u → u ∈ f ⊓ g`.
Also renames lots of lemmas to remove the word "sets" that was a remnant of the very early days.
In passing I also changed the simp lemma `filter.mem_map` from `t ∈ map m f ↔ {x | m x ∈ t} ∈ f` to
`t ∈ map m f ↔ m ⁻¹' t ∈ f` which seemed more normal form to me. But this led to a lot of breakage, so I also kept the old version as `mem_map'`.
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
