congr lemmas

Stream: general

[Yury G. Kudryashov]

It would be nice if someone who understand how @[congr] works will write a docstring. E.g., why this lemma can't be a @[congr] lemma?

[Eric Wieser]

A better link, yours goes to a collapsed file so the anchor doesn't work