Def Mathlib.Tactic.Order.collectFactsImp

Modification history

2025-10-14 16:26
Mathlib/Tactic/Order/CollectFacts.lean
feat(Tactic/Order): frontend for `order` (#27066) …
Deleted Mathlib.Tactic.Order.collectFactsImpView on Github →
2025-07-12 10:50
Mathlib/Tactic/Order/CollectFacts.lean
feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations (#26354) …
Modified Mathlib.Tactic.Order.collectFactsImpView on Github →
2025-02-26 07:29
Mathlib/Tactic/Order/CollectFacts.lean
feat(Tactic): `order` tactic for `Preorder`, `PartialOrder`, `LinearOrder` (#21877) …
Added Mathlib.Tactic.Order.collectFactsImpView on Github →