Commit 2022-09-15 01:42 a4895002

View on Github →

feat(data/sym/basic): add fill_mem, append_mem and supporting lemmas (#16486) Add lemmas for membership of fill and append, with supporting coercion and casting lemmas.

Estimated changes

Modified src/data/sym/basic.lean

modified def sym.append

modified theorem sym.append_comm

modified theorem sym.append_inj_left

modified theorem sym.append_inj_right

modified theorem sym.cast_cast

added theorem sym.coe_append

modified theorem sym.coe_cast

modified def sym.filter_ne

added theorem sym.mem_append_iff

added theorem sym.mem_cast

added theorem sym.mem_coe

modified theorem sym.mem_cons

modified theorem sym.mem_cons_of_mem

added theorem sym.mem_fill_iff