Commit 2026-07-28 13:45 5b1613e1

chore: reduce the abuse of the defeq Set α := α → Prop (#42169) All these changes fix issues of the form "A function is expecting Set α but is given α → Prop, or vice-versa". Generated by Claude Opus, then reviewed and cherry-picked line-by-line by myself. Assisted-by: Claude Opus 4.8