mathlib

df4066cf - refactor(order/ideal): Make `order.ideal` extend `lower_set` (#13070)

refactor(order/ideal): Make `order.ideal` extend `lower_set` (#13070) * Redefine `order.ideal` to extend `lower_set`. * `set_like` instance * Get rid of `order.ideal.ideal_Inter_nonempty` in favor of `order_bot` * Make arguments to `order.ideal.sup_mem` semi-implicit * Reorder sections according to typeclass assumptions (some were outdated since Yakov's `order_bot`/`order_top` refactor)