basic): add `fill_mem`, `append_mem` and supporting lemmas (#16486)

Commit

3 years ago

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.

Author

pimotte

Parents

fd2fb7b3

mathlib3 a4895002 - feat(data/sym/basic): add `fill_mem`, `append_mem` and supporting lemmas (#16486)

mathlib3
a4895002 - feat(data/sym/basic): add `fill_mem`, `append_mem` and supporting lemmas (#16486)