Commit 2022-04-15 17:09 0c2d68a0

View on Github →

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.)

Estimated changes

Modified src/data/sym/sym2.lean

modified theorem sym2.map_comp

added theorem sym2.map_congr

added theorem sym2.map_id'

modified theorem sym2.map_id

added theorem sym2.mem_map