PR #10643 feat(data/set_like/basic): add a congr lemma

feat(data/set_like/basic): add a congr lemma #10643

eric-wieser wants to merge 2 commits into master from eric-wieser/set_like.dep_congr

feat(data/set_like/basic): add a congr lemma

2b0f9691

eric-wieser added WIP

gebner commented on 2021-12-06

Update basic.lean

9a1ed122

eric-wieser removed WIP

eric-wieser added awaiting-review

eric-wieser added RFC

jcommelin requested a review from

gebner 4 years ago

ericrbg commented on 2021-12-18

jcommelin removed awaiting-review

kim-em added too-late

Reviewers

ericrbg

jcommelin

gebner

Assignees

No one assigned

Labels

RFC too-late

Milestone

No milestone