Theorem filter.lift_lift'_same_le_lift'

refactor(order/filter): move lift and lift' to separate file

construct reals as complete, linear ordered field

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

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