Theorem tendsto_of_nat_at_top_at_top

refactor(order/filter): generalize map_succ_at_top_eq to arbitrary Galois insertions; generalize tendsto_coe_iff to arbitary order-preserving embeddings

feat(analysis/measure_theory): optimize proofs; trim, is_complete