Theorem GCongr.ssuperset_imp_ssuperset

Modification history

2026-07-06 15:50
Mathlib/Order/RelClasses.lean
feat: use `LE.le` for subset relation in `Set`, `Finset`, `PSet`, `ZFSet`, `Class` (#32983) …
Deleted GCongr.ssuperset_imp_ssupersetView on Github →
2025-06-13 14:34
Mathlib/Order/RelClasses.lean
chore(grewrite): import `gcongr` and `grewrite` in `Tactic.Common` (#25773) …
Added GCongr.ssuperset_imp_ssupersetView on Github →