Theorem Mathlib.Tactic.GCongr.gt_imp_gt_right

Modification history

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_gt_rightView 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_gt_rightView on Github →