chore(order/basic): add monotone.order_dual, `strict_mono.order_dua…

…l` (#2778)

Also split long lines and lint.

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

scripts/nolints.txt

@@ -1999,25 +1999,7 @@ apply_nolint pell.xz doc_blame
 apply_nolint pell.yz doc_blame
 
 -- order/basic.lean
-apply_nolint classical.DLO doc_blame
 apply_nolint decidable_linear_order_of_is_well_order doc_blame
-apply_nolint dense_or_discrete ge_or_gt
-apply_nolint directed_order doc_blame
-apply_nolint ge.is_antisymm ge_or_gt
-apply_nolint ge.is_linear_order ge_or_gt
-apply_nolint ge.is_partial_order ge_or_gt
-apply_nolint ge.is_preorder ge_or_gt
-apply_nolint ge.is_refl ge_or_gt
-apply_nolint ge.is_total ge_or_gt
-apply_nolint ge.is_total_preorder ge_or_gt
-apply_nolint ge.is_trans ge_or_gt
-apply_nolint ge_of_eq ge_or_gt
-apply_nolint gt.is_antisymm ge_or_gt
-apply_nolint gt.is_asymm ge_or_gt
-apply_nolint gt.is_irrefl ge_or_gt
-apply_nolint gt.is_strict_order ge_or_gt
-apply_nolint gt.is_trans ge_or_gt
-apply_nolint gt.is_trichotomous ge_or_gt
 apply_nolint well_founded.succ doc_blame
 apply_nolint well_founded.sup doc_blame
 
@@ -3094,4 +3076,4 @@ apply_nolint uniform_space.separation_setoid doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/order/basic.lean

@@ -52,6 +52,7 @@ preorder, order, partial order, linear order, monotone, strictly monotone
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w} {r : α → α → Prop}
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem ge_of_eq [preorder α] {a b : α} : a = b → a ≥ b :=
 λ h, h ▸ le_refl a
 
@@ -83,33 +84,48 @@ lemma antisymm_of_asymm (r) [is_asymm α r] : is_antisymm α r :=
 
 /- Convert algebraic structure style to explicit relation style typeclasses -/
 instance [preorder α] : is_refl α (≤) := ⟨le_refl⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_refl α (≥) := is_refl.swap _
 instance [preorder α] : is_trans α (≤) := ⟨@le_trans _ _⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_trans α (≥) := is_trans.swap _
 instance [preorder α] : is_preorder α (≤) := {}
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_preorder α (≥) := {}
 instance [preorder α] : is_irrefl α (<) := ⟨lt_irrefl⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_irrefl α (>) := is_irrefl.swap _
 instance [preorder α] : is_trans α (<) := ⟨@lt_trans _ _⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_trans α (>) := is_trans.swap _
 instance [preorder α] : is_asymm α (<) := ⟨@lt_asymm _ _⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_asymm α (>) := is_asymm.swap _
 instance [preorder α] : is_antisymm α (<) := antisymm_of_asymm _
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_antisymm α (>) := antisymm_of_asymm _
 instance [preorder α] : is_strict_order α (<) := {}
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [preorder α] : is_strict_order α (>) := {}
 instance preorder.is_total_preorder [preorder α] [is_total α (≤)] : is_total_preorder α (≤) := {}
 instance [partial_order α] : is_antisymm α (≤) := ⟨@le_antisymm _ _⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [partial_order α] : is_antisymm α (≥) := is_antisymm.swap _
 instance [partial_order α] : is_partial_order α (≤) := {}
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [partial_order α] : is_partial_order α (≥) := {}
 instance [linear_order α] : is_total α (≤) := ⟨le_total⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [linear_order α] : is_total α (≥) := is_total.swap _
-instance linear_order.is_total_preorder [linear_order α] : is_total_preorder α (≤) := by apply_instance
+instance linear_order.is_total_preorder [linear_order α] : is_total_preorder α (≤) :=
+  by apply_instance
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [linear_order α] : is_total_preorder α (≥) := {}
 instance [linear_order α] : is_linear_order α (≤) := {}
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [linear_order α] : is_linear_order α (≥) := {}
 instance [linear_order α] : is_trichotomous α (<) := ⟨lt_trichotomy⟩
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 instance [linear_order α] : is_trichotomous α (>) := is_trichotomous.swap _
 
 theorem preorder.ext {α} {A B : preorder α}
@@ -291,17 +307,23 @@ instance pi.preorder {ι : Type u} {α : ι → Type v} [∀i, preorder (α i)]
   le_refl  := assume a i, le_refl (a i),
   le_trans := assume a b c h₁ h₂ i, le_trans (h₁ i) (h₂ i) }
 
-instance pi.partial_order {ι : Type u} {α : ι → Type v} [∀i, partial_order (α i)] : partial_order (Πi, α i) :=
+instance pi.partial_order {ι : Type u} {α : ι → Type v} [∀i, partial_order (α i)] :
+  partial_order (Πi, α i) :=
 { le_antisymm := λf g h1 h2, funext (λb, le_antisymm (h1 b) (h2 b)),
   ..pi.preorder }
 
 theorem comp_le_comp_left_of_monotone [preorder α] [preorder β]
-  {f : β → α} {g h : γ → β} (m_f : monotone f) (le_gh : g ≤ h) : has_le.le.{max w u} (f ∘ g) (f ∘ h) :=
+  {f : β → α} {g h : γ → β} (m_f : monotone f) (le_gh : g ≤ h) :
+  has_le.le.{max w u} (f ∘ g) (f ∘ h) :=
 assume x, m_f (le_gh x)
 
 section monotone
 variables [preorder α] [preorder γ]
 
+theorem monotone.order_dual {f : α → γ} (hf : monotone f) :
+  @monotone (order_dual α) (order_dual γ) _ _ f :=
+λ x y hxy, hf hxy
+
 theorem monotone_lam {f : α → β → γ} (m : ∀b, monotone (λa, f a b)) : monotone f :=
 assume a a' h b, m b h
 
@@ -310,6 +332,10 @@ assume a a' h, m h b
 
 end monotone
 
+theorem strict_mono.order_dual [has_lt α] [has_lt β] {f : α → β} (hf : strict_mono f) :
+  @strict_mono (order_dual α) (order_dual β) _ _ f :=
+λ x y hxy, hf hxy
+
 /-- Transfer a `preorder` on `β` to a `preorder` on `α` using a function `f : α → β`. -/
 def preorder.lift {α β} (f : α → β) (i : preorder β) : preorder α :=
 by exactI
@@ -346,7 +372,8 @@ by exactI
 instance subtype.preorder {α} [i : preorder α] (p : α → Prop) : preorder (subtype p) :=
 preorder.lift subtype.val i
 
-instance subtype.partial_order {α} [i : partial_order α] (p : α → Prop) : partial_order (subtype p) :=
+instance subtype.partial_order {α} [i : partial_order α] (p : α → Prop) :
+  partial_order (subtype p) :=
 partial_order.lift subtype.val subtype.val_injective i
 
 instance subtype.linear_order {α} [i : linear_order α] (p : α → Prop) : linear_order (subtype p) :=
@@ -411,7 +438,8 @@ instance order_dual.densely_ordered (α : Type u) [preorder α] [densely_ordered
   densely_ordered (order_dual α) :=
 ⟨λ a₁ a₂ ha, (@dense α _ _ _ _ ha).imp $ λ a, and.symm⟩
 
-lemma le_of_forall_le_of_dense [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀a₃>a₂, a₁ ≤ a₃) :
+lemma le_of_forall_le_of_dense [linear_order α] [densely_ordered α] {a₁ a₂ : α}
+  (h : ∀a₃>a₂, a₁ ≤ a₃) :
   a₁ ≤ a₂ :=
 le_of_not_gt $ assume ha,
   let ⟨a, ha₁, ha₂⟩ := dense ha in
@@ -421,7 +449,8 @@ lemma eq_of_le_of_forall_le_of_dense [linear_order α] [densely_ordered α] {a
   (h₁ : a₂ ≤ a₁) (h₂ : ∀a₃>a₂, a₁ ≤ a₃) : a₁ = a₂ :=
 le_antisymm (le_of_forall_le_of_dense h₂) h₁
 
-lemma le_of_forall_ge_of_dense [linear_order α] [densely_ordered α] {a₁ a₂ : α}(h : ∀a₃<a₁, a₂ ≥ a₃) :
+lemma le_of_forall_ge_of_dense [linear_order α] [densely_ordered α] {a₁ a₂ : α}
+  (h : ∀a₃<a₁, a₂ ≥ a₃) :
   a₁ ≤ a₂ :=
 le_of_not_gt $ assume ha,
   let ⟨a, ha₁, ha₂⟩ := dense ha in
@@ -431,6 +460,7 @@ lemma eq_of_le_of_forall_ge_of_dense [linear_order α] [densely_ordered α] {a
   (h₁ : a₂ ≤ a₁) (h₂ : ∀a₃<a₁, a₂ ≥ a₃) : a₁ = a₂ :=
 le_antisymm (le_of_forall_ge_of_dense h₂) h₁
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 lemma dense_or_discrete [linear_order α] (a₁ a₂ : α) :
   (∃a, a₁ < a ∧ a < a₂) ∨ ((∀a>a₁, a ≥ a₂) ∧ (∀a<a₂, a ≤ a₁)) :=
 classical.or_iff_not_imp_left.2 $ assume h,
@@ -483,7 +513,8 @@ section prio
 set_option default_priority 100 -- see Note [default priority]
 /-- This is basically the same as `is_strict_total_order`, but that definition is
   in Type (probably by mistake) and also has redundant assumptions. -/
-@[algebra] class is_strict_total_order' (α : Type u) (lt : α → α → Prop) extends is_trichotomous α lt, is_strict_order α lt : Prop.
+@[algebra] class is_strict_total_order' (α : Type u) (lt : α → α → Prop)
+  extends is_trichotomous α lt, is_strict_order α lt : Prop.
 end prio
 
 /-- Construct a linear order from a `is_strict_total_order'` relation -/
@@ -497,15 +528,19 @@ def linear_order_of_STO' (r) [is_strict_total_order' α r] : linear_order α :=
   ..partial_order_of_SO r }
 
 /-- Construct a decidable linear order from a `is_strict_total_order'` relation -/
-def decidable_linear_order_of_STO' (r) [is_strict_total_order' α r] [decidable_rel r] : decidable_linear_order α :=
+def decidable_linear_order_of_STO' (r) [is_strict_total_order' α r] [decidable_rel r] :
+  decidable_linear_order α :=
 by letI LO := linear_order_of_STO' r; exact
 { decidable_le := λ x y, decidable_of_iff (¬ r y x) (@not_lt _ _ y x),
   ..LO }
 
+/-- Any `linear_order` is a noncomputable `decidable_linear_order`. This is not marked
+as an instance to avoid a loop. -/
 noncomputable def classical.DLO (α) [LO : linear_order α] : decidable_linear_order α :=
 { decidable_le := classical.dec_rel _, ..LO }
 
-theorem is_strict_total_order'.swap (r) [is_strict_total_order' α r] : is_strict_total_order' α (swap r) :=
+theorem is_strict_total_order'.swap (r) [is_strict_total_order' α r] :
+  is_strict_total_order' α (swap r) :=
 {..is_trichotomous.swap r, ..is_strict_order.swap r}
 
 instance [linear_order α] : is_strict_total_order' α (<) := {}
@@ -560,23 +595,31 @@ instance is_extensional_of_is_strict_total_order'
 section prio
 set_option default_priority 100 -- see Note [default priority]
 /-- A well order is a well-founded linear order. -/
-@[algebra] class is_well_order (α : Type u) (r : α → α → Prop) extends is_strict_total_order' α r : Prop :=
+@[algebra] class is_well_order (α : Type u) (r : α → α → Prop)
+  extends is_strict_total_order' α r : Prop :=
 (wf : well_founded r)
 end prio
 
 @[priority 100] -- see Note [lower instance priority]
-instance is_well_order.is_strict_total_order {α} (r : α → α → Prop) [is_well_order α r] : is_strict_total_order α r := by apply_instance
+instance is_well_order.is_strict_total_order {α} (r : α → α → Prop) [is_well_order α r] :
+  is_strict_total_order α r := by apply_instance
 @[priority 100] -- see Note [lower instance priority]
-instance is_well_order.is_extensional {α} (r : α → α → Prop) [is_well_order α r] : is_extensional α r := by apply_instance
+instance is_well_order.is_extensional {α} (r : α → α → Prop) [is_well_order α r] :
+  is_extensional α r := by apply_instance
 @[priority 100] -- see Note [lower instance priority]
-instance is_well_order.is_trichotomous {α} (r : α → α → Prop) [is_well_order α r] : is_trichotomous α r := by apply_instance
+instance is_well_order.is_trichotomous {α} (r : α → α → Prop) [is_well_order α r] :
+  is_trichotomous α r := by apply_instance
 @[priority 100] -- see Note [lower instance priority]
-instance is_well_order.is_trans {α} (r : α → α → Prop) [is_well_order α r] : is_trans α r := by apply_instance
+instance is_well_order.is_trans {α} (r : α → α → Prop) [is_well_order α r] :
+  is_trans α r := by apply_instance
 @[priority 100] -- see Note [lower instance priority]
-instance is_well_order.is_irrefl {α} (r : α → α → Prop) [is_well_order α r] : is_irrefl α r := by apply_instance
+instance is_well_order.is_irrefl {α} (r : α → α → Prop) [is_well_order α r] :
+  is_irrefl α r := by apply_instance
 @[priority 100] -- see Note [lower instance priority]
-instance is_well_order.is_asymm {α} (r : α → α → Prop) [is_well_order α r] : is_asymm α r := by apply_instance
+instance is_well_order.is_asymm {α} (r : α → α → Prop) [is_well_order α r] :
+  is_asymm α r := by apply_instance
 
+/-- Construct a decidable linear order from a well-founded linear order. -/
 noncomputable def decidable_linear_order_of_is_well_order (r : α → α → Prop) [is_well_order α r] :
   decidable_linear_order α :=
 by { haveI := linear_order_of_STO' r, exact classical.DLO α }
@@ -589,13 +632,15 @@ instance empty_relation.is_well_order [subsingleton α] : is_well_order α empty
 
 instance nat.lt.is_well_order : is_well_order ℕ (<) := ⟨nat.lt_wf⟩
 
-instance sum.lex.is_well_order [is_well_order α r] [is_well_order β s] : is_well_order (α ⊕ β) (sum.lex r s) :=
+instance sum.lex.is_well_order [is_well_order α r] [is_well_order β s] :
+  is_well_order (α ⊕ β) (sum.lex r s) :=
 { trichotomous := λ a b, by cases a; cases b; simp; apply trichotomous,
   irrefl       := λ a, by cases a; simp; apply irrefl,
   trans        := λ a b c, by cases a; cases b; simp; cases c; simp; apply trans,
   wf           := sum.lex_wf is_well_order.wf is_well_order.wf }
 
-instance prod.lex.is_well_order [is_well_order α r] [is_well_order β s] : is_well_order (α × β) (prod.lex r s) :=
+instance prod.lex.is_well_order [is_well_order α r] [is_well_order β s] :
+  is_well_order (α × β) (prod.lex r s) :=
 { trichotomous := λ ⟨a₁, a₂⟩ ⟨b₁, b₂⟩,
     match @trichotomous _ r _ a₁ b₁ with
     | or.inl h₁ := or.inl $ prod.lex.left _ _ h₁
@@ -633,7 +678,7 @@ end
 by { classical, rw [not_iff_comm, not_bounded_iff] }
 
 namespace well_founded
-/-- If `r` is a well founded relation, then any nonempty set has a minimum element
+/-- If `r` is a well-founded relation, then any nonempty set has a minimum element
 with respect to `r`. -/
 theorem has_min {α} {r : α → α → Prop} (H : well_founded r)
   (s : set α) : s.nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬ r x a
@@ -654,6 +699,7 @@ theorem not_lt_min {α} {r : α → α → Prop} (H : well_founded r)
 let ⟨_, h'⟩ := classical.some_spec (H.has_min p h) in h' _ xp
 
 open set
+/-- The supremum of a bounded, well-founded order -/
 protected noncomputable def sup {α} {r : α → α → Prop} (wf : well_founded r) (s : set α)
   (h : bounded r s) : α :=
 wf.min { x | ∀a ∈ s, r a x } h
@@ -664,6 +710,8 @@ min_mem wf { x | ∀a ∈ s, r a x } h x hx
 
 section
 open_locale classical
+/-- The successor of an element `x` in a well-founded order is the minimum element `y` such that
+`x < y` if one exists. Otherwise it is `x` itself. -/
 protected noncomputable def succ {α} {r : α → α → Prop} (wf : well_founded r) (x : α) : α :=
 if h : ∃y, r x y then wf.min { y | r x y } h else x
 
@@ -727,6 +775,8 @@ theorem directed.mono_comp {ι} {rb : β → β → Prop} {g : α → β} {f : 
 
 section prio
 set_option default_priority 100 -- see Note [default priority]
+/-- A `preorder` is a `directed_order` if for any two elements `i`, `j`
+there is an element `k` such that `i ≤ k` and `j ≤ k`. -/
 class directed_order (α : Type u) extends preorder α :=
 (directed : ∀ i j : α, ∃ k, i ≤ k ∧ j ≤ k)
 end prio