Theorem GCongr.ssuperset_imp_ssuperset_left

Modification history

2025-07-31 09:17
Mathlib/Order/RelClasses.lean
feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) …
Deleted GCongr.ssuperset_imp_ssuperset_leftView on Github →
2025-06-16 13:31
Mathlib/Order/RelClasses.lean
chore: whitespace fixes (#25956) …
Modified GCongr.ssuperset_imp_ssuperset_leftView 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_ssuperset_leftView on Github →