Commit 2026-09-24 14:17 b3b63681
View on Github →feat: IsConcreteLE (Set α) α (#44119)
Add an instance of IsConcreteLE (Set α) α. This makes it so that mem_of_le_of_mem supersedes Set.mem_of_subset_of_mem, so only mem_of_le_of_mem needs to be @[gcongr].