Commit 2026-10-27 23:51 c63d9df9

feat: tag Metric.closedBall_subset_ball with @[gcongr strict] (#43419) This PR uses @[gcongr strict] on Metric.closedBall_subset_ball so that it can be used by gcongr and grw. This means that we will be able to rewrite with a strict inequality to turn a closed ball into an open ball or vice versa. I golfed away some uses of Metric.closedBall_subset_ball using grw. To aid this, I also added some more @[gcongr] attributes.