Commit 2024-07-31 18:23 0a717792
View on Github →chore: remove obsolete comments about @[congr] (#15299) Some of these have been commented out since this file was added to mathlib 3, others refer to theorems that have been upstreamed. In any case, they are not actionable.