feat: port Init.Data.Ordering.Lemmas (#4281)

Mathlib.lean

@@ -1537,6 +1537,7 @@ import Mathlib.Init.Data.Option.Basic
 import Mathlib.Init.Data.Option.Init.Lemmas
 import Mathlib.Init.Data.Option.Lemmas
 import Mathlib.Init.Data.Ordering.Basic
+import Mathlib.Init.Data.Ordering.Lemmas
 import Mathlib.Init.Data.Prod
 import Mathlib.Init.Data.Quot
 import Mathlib.Init.Data.Rat.Basic

Mathlib/Init/Data/Ordering/Lemmas.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+! This file was ported from Lean 3 source module init.data.ordering.lemmas
+! leanprover-community/lean commit 4bd314f7bd5e0c9e813fc201f1279a23f13f9f1d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+
+import Mathlib.Init.Data.Ordering.Basic
+import Mathlib.Init.Algebra.Classes
+import Mathlib.Init.IteSimp
+
+/-!
+# Some `Ordering` lemmas
+-/
+
+universe u
+
+namespace Ordering
+
+@[simp]
+theorem ite_eq_lt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
+    ((if c then a else b) = Ordering.lt) = if c then a = Ordering.lt else b = Ordering.lt := by
+  by_cases c <;> simp [*]
+#align ordering.ite_eq_lt_distrib Ordering.ite_eq_lt_distrib
+
+@[simp]
+theorem ite_eq_eq_distrib (c : Prop) [Decidable c] (a b : Ordering) :
+    ((if c then a else b) = Ordering.eq) = if c then a = Ordering.eq else b = Ordering.eq := by
+  by_cases c <;> simp [*]
+#align ordering.ite_eq_eq_distrib Ordering.ite_eq_eq_distrib
+
+@[simp]
+theorem ite_eq_gt_distrib (c : Prop) [Decidable c] (a b : Ordering) :
+    ((if c then a else b) = Ordering.gt) = if c then a = Ordering.gt else b = Ordering.gt := by
+  by_cases c <;> simp [*]
+#align ordering.ite_eq_gt_distrib Ordering.ite_eq_gt_distrib
+
+end Ordering
+
+section
+
+variable {α : Type u} {lt : α → α → Prop} [DecidableRel lt]
+
+attribute [local simp] cmpUsing
+
+@[simp]
+theorem cmpUsing_eq_lt (a b : α) : (cmpUsing lt a b = Ordering.lt) = lt a b := by simp
+#align cmp_using_eq_lt cmpUsing_eq_lt
+
+@[simp]
+theorem cmpUsing_eq_gt [IsStrictOrder α lt] (a b : α) :
+    (cmpUsing lt a b = Ordering.gt) = lt b a := by
+  simp only [cmpUsing, Ordering.ite_eq_gt_distrib, if_false_right_eq_and, and_true,
+    if_false_left_eq_and]
+  apply propext
+  apply Iff.intro
+  · exact fun h => h.2
+  · intro hba
+    constructor
+    · intro hab
+      exact absurd (_root_.trans hab hba) (irrefl a)
+    · assumption
+#align cmp_using_eq_gt cmpUsing_eq_gt
+
+@[simp]
+theorem cmpUsing_eq_eq (a b : α) : (cmpUsing lt a b = Ordering.eq) = (¬lt a b ∧ ¬lt b a) := by simp
+#align cmp_using_eq_eq cmpUsing_eq_eq
+
+end