Commit 2025-12-05 15:16 fcef8981

View on Github →

chore(Tactic/Order): use AtomM (#31673) The order tactic uses its own machinery to collect atoms and facts from the context. This PR replaces it with AtomM to unify with other tactics like ring.

Estimated changes

Modified Mathlib/Tactic/Order.lean

modified def Mathlib.Tactic.Order.findContradictionWithNe

modified def Mathlib.Tactic.Order.findContradictionWithNle

modified def Mathlib.Tactic.Order.orderCore

added def Mathlib.Tactic.Order.orderCoreImp

modified def Mathlib.Tactic.Order.updateGraphWithNltInfSup

Modified Mathlib/Tactic/Order/CollectFacts.lean

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

modified def Mathlib.Tactic.Order.Graph.buildTransitiveLeProof

modified def Mathlib.Tactic.Order.Graph.constructLeGraph

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

modified def Mathlib.Tactic.Order.Graph.findSCCs

Modified Mathlib/Tactic/Order/Preprocessing.lean

modified def Mathlib.Tactic.Order.preprocessFacts

modified def Mathlib.Tactic.Order.preprocessFactsLinear

modified def Mathlib.Tactic.Order.preprocessFactsPartial

modified def Mathlib.Tactic.Order.replaceBotTop

Modified Mathlib/Tactic/Order/ToInt.lean

Modified Mathlib/Util/AtomM.lean

modified def Mathlib.Tactic.AtomM.addAtom

added def Mathlib.Tactic.AtomM.containsThenAdd

added def Mathlib.Tactic.AtomM.containsThenAddQ

Modified MathlibTest/order.lean