Commit 2025-07-11 15:56 325f7894

chore: Add grind tags for Set.mem_Ixx (#26571) This adds grind tags to the various Set.mem_Ixx lemmas, which should let the grind linarith module discharge goals of this form. I went with the convervative option of only including the grind = pattern, which only fires on the LHS of these lemmas. One could also consider having patterns going the other way as well (i.e. grind _=_ for mem_Ioi or multi-patterns for mem_Ioo and so on).