Theorem filter.map_swap_vmap_swap_eq

chore(order/filter): simplify definition of filter.prod; cleanup

construct reals as complete, linear ordered field

refactor(*): use 'lemma' iff statement is private

refactor(*): import content from lean/library/data and library_dev