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

Commit

4 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

Committer

b-mehta

Parents

4036f521

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

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