Provide "lookup" and commuting lemmas as equations that always apply, and fix some inconsistent lemma naming

!507 (closed) ballooned into this huge change. This contains the following two MRs:

• !526 (merged)
• !531 (merged)

There is more that could be done, but that is postponed (we should probably open an issue):

• non_empty change as discussed in !526 (comment 97794)
• Direction of equality in fmap/omap/alter lemmas, see !531 (comment 97789)