mathlib

0c2d68a0 - feat(data/sym/sym2): mem_map/mem_congr/map_id' (#13437)

feat(data/sym/sym2): mem_map/mem_congr/map_id' (#13437) Additional simplification lemmas, one to address non-simp-normal-form. (Also did a few proof simplifications.)