chore(data/pi/lex): turn pi.lex.linear_order into an instance (#14389)

* Use `[is_well_order ι (<)]` instead of `(wf : well_founded ((<) : ι → ι → Prop))`. This way `pi.lex.linear_order` can be an instance.
* Add `pi.lex.order_bot`/`pi.lex.order_top`/`pi.lex.bounded_order`.

src/data/pi/lex.lean

@@ -46,6 +46,23 @@ notation `Πₗ` binders `, ` r:(scoped p, lex (Π i, p i)) := r
 @[simp] lemma to_lex_apply (x : Π i, β i) (i : ι) : to_lex x i = x i := rfl
 @[simp] lemma of_lex_apply (x : lex (Π i, β i)) (i : ι) : of_lex x i = x i := rfl
 
+lemma is_trichotomous_lex [∀ i, is_trichotomous (β i) s] (wf : well_founded r) :
+  is_trichotomous (Π i, β i) (pi.lex r @s) :=
+{ trichotomous := λ a b,
+    begin
+      cases eq_or_ne a b with hab hab,
+      { exact or.inr (or.inl hab) },
+      { rw function.ne_iff at hab,
+        let i := wf.min _ hab,
+        have hri : ∀ j, r j i → a j = b j,
+        { intro j, rw ← not_imp_not,
+          exact λ h', wf.not_lt_min _ _ h' },
+        have hne : a i ≠ b i, from wf.min_mem _ hab,
+        cases trichotomous_of s (a i) (b i) with hi hi,
+        exacts [or.inl ⟨i, hri, hi⟩,
+          or.inr $ or.inr $ ⟨i, λ j hj, (hri j hj).symm, hi.resolve_left hne⟩] },
+    end }
+
 instance [has_lt ι] [Π a, has_lt (β a)] : has_lt (lex (Π i, β i)) := ⟨pi.lex (<) (λ _, (<))⟩
 
 instance lex.is_strict_order [linear_order ι] [∀ a, partial_order (β a)] :
@@ -63,36 +80,37 @@ instance lex.is_strict_order [linear_order ι] [∀ a, partial_order (β a)] :
 instance [linear_order ι] [Π a, partial_order (β a)] : partial_order (lex (Π i, β i)) :=
 partial_order_of_SO (<)
 
-protected lemma lex.is_strict_total_order' [linear_order ι]
-  (wf : well_founded ((<) : ι → ι → Prop)) [∀ a, linear_order (β a)] :
-  is_strict_total_order' (lex (Π i, β i)) (<) :=
-{ trichotomous := λ a b,
-    begin
-      by_cases h : ∃ i, a i ≠ b i,
-      { let i := wf.min _ h,
-        have hlt_i : ∀ j < i, a j = b j,
-        { intro j, rw ← not_imp_not,
-          exact λ h', wf.not_lt_min _ _ h' },
-        have : a i ≠ b i, from wf.min_mem _ h,
-        exact this.lt_or_lt.imp (λ h, ⟨i, hlt_i, h⟩)
-          (λ h, or.inr ⟨i, λ j hj, (hlt_i j hj).symm, h⟩) },
-      { push_neg at h, exact or.inr (or.inl (funext h)) }
-    end }
-
-/-- `Πₗ i, α i` is a linear order if the original order is well-founded.
-This cannot be an instance, since it depends on the well-foundedness of `<`. -/
-protected noncomputable def lex.linear_order [linear_order ι]
-  (wf : well_founded ((<) : ι → ι → Prop)) [∀ a, linear_order (β a)] :
+/-- `Πₗ i, α i` is a linear order if the original order is well-founded. -/
+noncomputable instance [linear_order ι] [is_well_order ι (<)] [∀ a, linear_order (β a)] :
   linear_order (lex (Π i, β i)) :=
-@linear_order_of_STO' (Πₗ i, β i) (<) (pi.lex.is_strict_total_order' wf) (classical.dec_rel _)
-
-lemma lex.le_of_forall_le [linear_order ι]
-  (wf : well_founded ((<) : ι → ι → Prop)) [Π a, linear_order (β a)] {a b : lex (Π i, β i)}
-  (h : ∀ i, a i ≤ b i) : a ≤ b :=
-begin
-  letI : linear_order (Πₗ i, β i) := lex.linear_order wf,
-  exact le_of_not_lt (λ ⟨i, hi⟩, (h i).not_lt hi.2)
-end
+@linear_order_of_STO' (Πₗ i, β i) (<)
+  { to_is_trichotomous := is_trichotomous_lex _ _ is_well_order.wf } (classical.dec_rel _)
+
+lemma lex.le_of_forall_le [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)]
+  {a b : lex (Π i, β i)} (h : ∀ i, a i ≤ b i) : a ≤ b :=
+le_of_not_lt (λ ⟨i, hi⟩, (h i).not_lt hi.2)
+
+lemma lex.le_of_of_lex_le [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)]
+  {a b : lex (Π i, β i)} (h : of_lex a ≤ of_lex b) : a ≤ b :=
+lex.le_of_forall_le h
+
+lemma to_lex_monotone [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)] :
+  monotone (@to_lex (Π i, β i)) :=
+λ _ _, lex.le_of_forall_le
+
+instance [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)]
+  [Π a, order_bot (β a)] : order_bot (lex (Π a, β a)) :=
+{ bot := to_lex ⊥,
+  bot_le := λ f, lex.le_of_of_lex_le bot_le }
+
+instance [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)]
+  [Π a, order_top (β a)] : order_top (lex (Π a, β a)) :=
+{ top := to_lex ⊤,
+  le_top := λ f, lex.le_of_of_lex_le le_top }
+
+instance [linear_order ι] [is_well_order ι (<)] [Π a, linear_order (β a)]
+  [Π a, bounded_order (β a)] : bounded_order (lex (Π a, β a)) :=
+{ .. pi.lex.order_bot, .. pi.lex.order_top }
 
 --we might want the analog of `pi.ordered_cancel_comm_monoid` as well in the future
 @[to_additive]