Def Mathlib.Tactic.GCongr.exactLeOfLt

Modification history

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.exactLeOfLtView on Github →
2025-06-13 14:34
Mathlib/Tactic/GCongr/Core.lean
chore(grewrite): import `gcongr` and `grewrite` in `Tactic.Common` (#25773) …
Deleted Mathlib.Tactic.GCongr.exactLeOfLtView on Github →
2023-06-15 06:25
Mathlib/Tactic/GCongr.lean
chore: move around `gcongr` material (#5067) …
Modified Mathlib.Tactic.GCongr.exactLeOfLtView on Github →
2023-06-05 08:37
Mathlib/Tactic/GCongr.lean
feat: tactic `gcongr` for "relational congruence" (#3965) …
Added Mathlib.Tactic.GCongr.exactLeOfLtView on Github →