Def Mathlib.Tactic.Order.findContradictionWithNe

Modification history

2025-12-05 15:16

Mathlib/Tactic/Order.lean

chore(Tactic/Order): use `AtomM` (#31673) …

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

2025-02-26 07:29

Mathlib/Tactic/Order.lean

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

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