Commit 2025-07-12 10:50 720505e5

View on Github →

feat(Tactic/Order): support ⊤, ⊥, and lattice operations (#26354) Support ⊤, ⊥, and lattice operations in the order tactic.

Estimated changes

Modified Mathlib/Tactic/Order.lean

deleted def Mathlib.Tactic.Order.updateGraphWithNlt

added def Mathlib.Tactic.Order.updateGraphWithNltInfSup

Modified Mathlib/Tactic/Order/CollectFacts.lean

modified def Mathlib.Tactic.Order.collectFacts

modified def Mathlib.Tactic.Order.collectFactsImp

Modified Mathlib/Tactic/Order/Graph/Basic.lean

modified def Mathlib.Tactic.Order.Graph.constructLeGraph

Modified Mathlib/Tactic/Order/Preprocessing.lean

modified def Mathlib.Tactic.Order.preprocessFactsLinear

modified def Mathlib.Tactic.Order.preprocessFactsPartial

modified def Mathlib.Tactic.Order.preprocessFactsPreorder

Modified MathlibTest/order.lean

Modified scripts/noshake.json