Commit 2026-11-10 16:49 e00dcc47

feat: @[gcongr] for eq_top_mono and friends (#44334) This PR tags lemma eq_top_mono and various similar lemmas with @[gcongr]. This lets us use grw in places where we couldn't before. The supported maximal/minimal constants are ⊤, ⊥, (∅ : Set _), Set.univ, 0, 1, each on either side of an equality = and an inequality ≠. subset_eq_empty is renamed to eq_empty_of_subset, to match eq_univ_of_subset. Performance note: @[gcongr] lemmas are indexed only by the relation and head constand, which for these lemmas is → and = or ≠. So, it will need to try all 12 available lemmas in these cases. I do not think that this will cause any noticeable performance issue. If it does, we can consider a more detailed indexing of @[gcongr] lemmas.