Theorem Mathlib.Tactic.GCongr.gt_imp_gt

Modification history

2025-11-13 17:14
Mathlib/Order/Basic.lean
feat(gcongr): use mdata instead of template (#30739) …
Deleted Mathlib.Tactic.GCongr.gt_imp_gtView on Github →
2025-07-31 09:17
Mathlib/Order/Basic.lean
feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) …
Added Mathlib.Tactic.GCongr.gt_imp_gtView on Github →
2025-06-13 14:34
Mathlib/Tactic/GCongr.lean
chore(grewrite): import `gcongr` and `grewrite` in `Tactic.Common` (#25773) …
Deleted Mathlib.Tactic.GCongr.gt_imp_gtView on Github →
2025-06-11 22:43
Mathlib/Tactic/GCongr.lean
feat: a `grw` tactic for rewriting using inequalities (#8167)
Added Mathlib.Tactic.GCongr.gt_imp_gtView on Github →