Commit 2025-11-20 23:27 2fc191a2
View on Github →feat: @[gcongr] for indicator_le_indicator_of_subset (#31847)
This PR tags indicator_le_indicator_of_subset and indicator_le_indicator_apply_of_subset with gcongr, and uses this to golf some proofs.
It may be possible to improve gcongr in the future so that we only need to tag one of the two lemmas with gcongr.