Def Mathlib.Tactic.Order.preprocessFactsLinear

Modification history

2025-07-12 10:50

Mathlib/Tactic/Order/Preprocessing.lean

feat(Tactic/Order): support `⊤`, `⊥`, and lattice operations (#26354) …

Modified Mathlib.Tactic.Order.preprocessFactsLinear View on Github →

2025-02-26 07:29

Mathlib/Tactic/Order/Preprocessing.lean

feat(Tactic): `order` tactic for `Preorder`, `PartialOrder`, `LinearOrder` (#21877) …

Added Mathlib.Tactic.Order.preprocessFactsLinear View on Github →