These are some lemmas from Perennial about "filter" on maps. Most are by me; map_filter_insert_not_delete is by @tchajed (original name: map_filter_insert_not_strong).
map_filter_insert_not_delete
map_filter_insert_not_strong