feat(Order/Basic): Add ltByCases API (#9114)

I noticed that `ltByCases` doesn't have any API, and it would be useful to have some when working trichotomously, especially if one wishes to define things trichotomously.

A non-dependent version is also defined.

Author: linesthatinterlace

Mathlib/Order/Basic.lean

@@ -238,7 +238,6 @@ theorem not_gt (h : x = y) : ¬y < x :=
 
 end Eq
 
-
 section
 
 variable [Preorder α] {a b : α}
@@ -676,6 +675,123 @@ instance Order.Preimage.decidable {α β} (f : α → β) (s : β → β → Pro
     DecidableRel (f ⁻¹'o s) := fun _ _ ↦ H _ _
 #align order.preimage.decidable Order.Preimage.decidable
 
+section ltByCases
+
+variable [LinearOrder α] {P : Sort*} {x y : α}
+
+@[simp]
+lemma ltByCases_lt (h : x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :
+    ltByCases x y h₁ h₂ h₃ = h₁ h := dif_pos h
+
+@[simp]
+lemma ltByCases_gt (h : y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :
+    ltByCases x y h₁ h₂ h₃ = h₃ h := (dif_neg h.not_lt).trans (dif_pos h)
+
+@[simp]
+lemma ltByCases_eq (h : x = y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} :
+    ltByCases x y h₁ h₂ h₃ = h₂ h := (dif_neg h.not_lt).trans (dif_neg h.not_gt)
+
+lemma ltByCases_not_lt (h : ¬ x < y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}
+    (p : ¬ y < x → x = y := fun h' => (le_antisymm (le_of_not_gt h') (le_of_not_gt h))) :
+    ltByCases x y h₁ h₂ h₃ = if h' : y < x then h₃ h' else h₂ (p h') := dif_neg h
+
+lemma ltByCases_not_gt (h : ¬ y < x) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}
+    (p : ¬ x < y → x = y := fun h' => (le_antisymm (le_of_not_gt h) (le_of_not_gt h'))) :
+    ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₂ (p h') :=
+  dite_congr rfl (fun _ => rfl) (fun _ => dif_neg h)
+
+lemma ltByCases_ne (h : x ≠ y) {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}
+    (p : ¬ x < y → y < x := fun h' => h.lt_or_lt.resolve_left h') :
+    ltByCases x y h₁ h₂ h₃ = if h' : x < y then h₁ h' else h₃ (p h') :=
+  dite_congr rfl (fun _ => rfl) (fun _ => dif_pos _)
+
+lemma ltByCases_comm {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}
+    (p : y = x → x = y := fun h' => h'.symm) :
+    ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁ := by
+  refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)
+  · rw [ltByCases_lt h, ltByCases_gt h]
+  · rw [ltByCases_eq h, ltByCases_eq h.symm, comp_apply]
+  · rw [ltByCases_lt h, ltByCases_gt h]
+
+lemma eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt {x' y' : α}
+    (ltc : (x < y) ↔ (x' < y')) (gtc : (y < x) ↔ (y' < x')) :
+    x = y ↔ x' = y' := by simp_rw [eq_iff_le_not_lt, ← not_lt, ltc, gtc]
+
+lemma ltByCases_rec {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} (p : P)
+    (hlt : (h : x < y) → h₁ h = p) (heq : (h : x = y) → h₂ h = p)
+    (hgt : (h : y < x) → h₃ h = p) :
+    ltByCases x y h₁ h₂ h₃ = p :=
+  ltByCases x y
+    (fun h => ltByCases_lt h ▸ hlt h)
+    (fun h => ltByCases_eq h ▸ heq h)
+    (fun h => ltByCases_gt h ▸ hgt h)
+
+lemma ltByCases_eq_iff {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P} {p : P} :
+    ltByCases x y h₁ h₂ h₃ = p ↔ (∃ h, h₁ h = p) ∨ (∃ h, h₂ h = p) ∨ (∃ h, h₃ h = p) := by
+  refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)
+  · simp only [ltByCases_lt, exists_prop_of_true, h, h.not_lt, not_false_eq_true,
+    exists_prop_of_false, or_false, h.ne]
+  · simp only [h, lt_self_iff_false, ltByCases_eq, not_false_eq_true,
+    exists_prop_of_false, exists_prop_of_true, or_false, false_or]
+  · simp only [ltByCases_gt, exists_prop_of_true, h, h.not_lt, not_false_eq_true,
+    exists_prop_of_false, false_or, h.ne']
+
+lemma ltByCases_congr {x' y' : α} {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}
+    {h₁' : x' < y' → P} {h₂' : x' = y' → P} {h₃' : y' < x' → P} (ltc : (x < y) ↔ (x' < y'))
+    (gtc : (y < x) ↔ (y' < x')) (hh'₁ : ∀ (h : x' < y'), h₁ (ltc.mpr h) = h₁' h)
+    (hh'₂ : ∀ (h : x' = y'), h₂ ((eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc).mpr h) = h₂' h)
+    (hh'₃ : ∀ (h : y' < x'), h₃ (gtc.mpr h) = h₃' h) :
+    ltByCases x y h₁ h₂ h₃ = ltByCases x' y' h₁' h₂' h₃' := by
+  refine ltByCases_rec _ (fun h => ?_) (fun h => ?_) (fun h => ?_)
+  · rw [ltByCases_lt (ltc.mp h), hh'₁]
+  · rw [eq_iff_eq_of_lt_iff_lt_of_gt_iff_gt ltc gtc] at h
+    rw [ltByCases_eq h, hh'₂]
+  · rw [ltByCases_gt (gtc.mp h), hh'₃]
+
+/-- Perform a case-split on the ordering of `x` and `y` in a decidable linear order,
+non-dependently. -/
+abbrev ltTrichotomy (x y : α) (p q r : P) := ltByCases x y (fun _ => p) (fun _ => q) (fun _ => r)
+
+variable {p q r s : P}
+
+@[simp]
+lemma ltTrichotomy_lt (h : x < y) : ltTrichotomy x y p q r = p := ltByCases_lt h
+
+@[simp]
+lemma ltTrichotomy_gt (h : y < x) : ltTrichotomy x y p q r = r := ltByCases_gt h
+
+@[simp]
+lemma ltTrichotomy_eq (h : x = y) : ltTrichotomy x y p q r = q := ltByCases_eq h
+
+lemma ltTrichotomy_not_lt (h : ¬ x < y) :
+    ltTrichotomy x y p q r = if y < x then r else q := ltByCases_not_lt h
+
+lemma ltTrichotomy_not_gt (h : ¬ y < x) :
+    ltTrichotomy x y p q r = if x < y then p else q := ltByCases_not_gt h
+
+lemma ltTrichotomy_ne (h : x ≠ y) :
+    ltTrichotomy x y p q r = if x < y then p else r := ltByCases_ne h
+
+lemma ltTrichotomy_comm : ltTrichotomy x y p q r = ltTrichotomy y x r q p := ltByCases_comm
+
+lemma ltTrichotomy_self {p : P} : ltTrichotomy x y p p p = p :=
+  ltByCases_rec p (fun _ => rfl) (fun _ => rfl) (fun _ => rfl)
+
+lemma ltTrichotomy_eq_iff : ltTrichotomy x y p q r = s ↔
+    (x < y ∧ p = s) ∨ (x = y ∧ q = s) ∨ (y < x ∧ r = s) := by
+  refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)
+  · simp only [ltTrichotomy_lt, false_and, true_and, or_false, h, h.not_lt, h.ne]
+  · simp only [ltTrichotomy_eq, false_and, true_and, or_false, false_or, h, lt_irrefl]
+  · simp only [ltTrichotomy_gt, false_and, true_and, false_or, h, h.not_lt, h.ne']
+
+lemma ltTrichotomy_congr {x' y' : α} {p' q' r' : P} (ltc : (x < y) ↔ (x' < y'))
+    (gtc : (y < x) ↔ (y' < x')) (hh'₁ : x' < y' → p = p')
+    (hh'₂ : x' = y' → q = q') (hh'₃ : y' < x' → r = r') :
+    ltTrichotomy x y p q r = ltTrichotomy x' y' p' q' r' :=
+  ltByCases_congr ltc gtc hh'₁ hh'₂ hh'₃
+
+end ltByCases
+
 /-! ### Order dual -/