mathlib3

7f208430 - chore(order/filter): rephrase filter.has_le (#1399)

chore(order/filter): rephrase filter.has_le (#1399) The goal of this tiny refactor is to prevent `filter.sets` leaking when proving a filter g is finer than another one f. We want the goal to be `s ∈ f → s ∈ g` instead of the definitionaly equivalent `s ∈ f.sets ∈ g.sets`