chore(order/*): generalisation linter (#13105)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/order/atoms.lean

@@ -125,7 +125,7 @@ or.elim (eq_top_or_eq_of_coatom_le ha le_sup_left) id
 
 end pairwise
 
-variables [partial_order α] {a : α}
+variables [preorder α] {a : α}
 
 @[simp]
 lemma is_coatom_dual_iff_is_atom [order_bot α] :
@@ -540,13 +540,13 @@ is_simple_order_iff_is_simple_order_order_dual.trans is_simple_order_iff_is_atom
 
 namespace set
 
-theorem is_simple_order_Iic_iff_is_atom [partial_order α] [bounded_order α] {a : α} :
+theorem is_simple_order_Iic_iff_is_atom [partial_order α] [order_bot α] {a : α} :
   is_simple_order (Iic a) ↔ is_atom a :=
 is_simple_order_iff_is_atom_top.trans $ and_congr (not_congr subtype.mk_eq_mk)
   ⟨λ h b ab, subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab),
     λ h ⟨b, hab⟩ hbotb, subtype.mk_eq_mk.2 (h b (subtype.mk_lt_mk.1 hbotb))⟩
 
-theorem is_simple_order_Ici_iff_is_coatom [partial_order α] [bounded_order α] {a : α} :
+theorem is_simple_order_Ici_iff_is_coatom [partial_order α] [order_top α] {a : α} :
   is_simple_order (Ici a) ↔ is_coatom a :=
 is_simple_order_iff_is_coatom_bot.trans $ and_congr (not_congr subtype.mk_eq_mk)
   ⟨λ h b ab, subtype.mk_eq_mk.1 (h ⟨b, le_of_lt ab⟩ ab),

src/order/conditionally_complete_lattice.lean

@@ -568,6 +568,15 @@ lemma finset.nonempty.sup'_id_eq_cSup {s : finset α} (hs : s.nonempty) :
   s.sup' hs id = Sup s :=
 by rw [hs.sup'_eq_cSup_image, image_id]
 
+/--Introduction rule to prove that b is the supremum of s: it suffices to check that
+1) b is an upper bound
+2) every other upper bound b' satisfies b ≤ b'.-/
+theorem cSup_eq_of_is_forall_le_of_forall_le_imp_ge (_ : s.nonempty)
+  (h_is_ub : ∀ a ∈ s, a ≤ b) (h_b_le_ub : ∀ub, (∀ a ∈ s, a ≤ ub) → (b ≤ ub)) : Sup s = b :=
+le_antisymm
+  (show Sup s ≤ b, from cSup_le ‹s.nonempty› h_is_ub)
+  (show b ≤ Sup s, from h_b_le_ub _ $ assume a, le_cSup ⟨b, h_is_ub⟩)
+
 end conditionally_complete_lattice
 
 instance pi.conditionally_complete_lattice {ι : Type*} {α : Π i : ι, Type*}
@@ -639,15 +648,6 @@ lemma exists_lt_of_cinfi_lt [nonempty ι] {f : ι → α} (h : infi f < a) :
   (∃i, f i < a) :=
 @exists_lt_of_lt_csupr (order_dual α) _ _ _ _ _ h
 
-/--Introduction rule to prove that b is the supremum of s: it suffices to check that
-1) b is an upper bound
-2) every other upper bound b' satisfies b ≤ b'.-/
-theorem cSup_eq_of_is_forall_le_of_forall_le_imp_ge (_ : s.nonempty)
-  (h_is_ub : ∀ a ∈ s, a ≤ b) (h_b_le_ub : ∀ub, (∀ a ∈ s, a ≤ ub) → (b ≤ ub)) : Sup s = b :=
-le_antisymm
-  (show Sup s ≤ b, from cSup_le ‹s.nonempty› h_is_ub)
-  (show b ≤ Sup s, from h_b_le_ub _ $ assume a, le_cSup ⟨b, h_is_ub⟩)
-
 open function
 variables [is_well_order α (<)]
 

src/order/lattice_intervals.lean

@@ -88,7 +88,7 @@ instance [preorder α] : order_top (Iic a) :=
 { top := ⟨a, le_refl a⟩,
   le_top := λ x, x.prop }
 
-@[simp] lemma coe_top [partial_order α] {a : α} : ↑(⊤ : Iic a) = a := rfl
+@[simp] lemma coe_top [preorder α] {a : α} : ↑(⊤ : Iic a) = a := rfl
 
 instance [preorder α] [order_bot α] : order_bot (Iic a) :=
 { bot := ⟨⊥, bot_le⟩,
@@ -123,7 +123,7 @@ instance [preorder α] : order_bot (Ici a) :=
 { bot := ⟨a, le_refl a⟩,
   bot_le := λ x, x.prop }
 
-@[simp] lemma coe_bot [partial_order α] {a : α} : ↑(⊥ : Ici a) = a := rfl
+@[simp] lemma coe_bot [preorder α] {a : α} : ↑(⊥ : Ici a) = a := rfl
 
 instance [preorder α] [order_top α] : order_top (Ici a) :=
 { top := ⟨⊤, le_top⟩,

src/order/modular_lattice.lean

@@ -86,7 +86,7 @@ theorem inf_lt_inf_of_lt_of_sup_le_sup (hxy : x < y) (hinf : y ⊔ z ≤ x ⊔ z
 /-- A generalization of the theorem that if `N` is a submodule of `M` and
   `N` and `M / N` are both Artinian, then `M` is Artinian. -/
 theorem well_founded_lt_exact_sequence
-  {β γ : Type*} [partial_order β] [partial_order γ]
+  {β γ : Type*} [partial_order β] [preorder γ]
   (h₁ : well_founded ((<) : β → β → Prop))
   (h₂ : well_founded ((<) : γ → γ → Prop))
   (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ)
@@ -110,7 +110,7 @@ subrelation.wf
 /-- A generalization of the theorem that if `N` is a submodule of `M` and
   `N` and `M / N` are both Noetherian, then `M` is Noetherian.  -/
 theorem well_founded_gt_exact_sequence
-  {β γ : Type*} [partial_order β] [partial_order γ]
+  {β γ : Type*} [preorder β] [partial_order γ]
   (h₁ : well_founded ((>) : β → β → Prop))
   (h₂ : well_founded ((>) : γ → γ → Prop))
   (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ)
@@ -165,7 +165,7 @@ instance [distrib_lattice α] : is_modular_lattice α :=
 end distrib_lattice
 
 theorem disjoint.disjoint_sup_right_of_disjoint_sup_left
-  [lattice α] [bounded_order α] [is_modular_lattice α] {a b c : α}
+  [lattice α] [order_bot α] [is_modular_lattice α] {a b c : α}
   (h : disjoint a b) (hsup : disjoint (a ⊔ b) c) :
   disjoint a (b ⊔ c) :=
 begin
@@ -176,7 +176,7 @@ begin
 end
 
 theorem disjoint.disjoint_sup_left_of_disjoint_sup_right
-  [lattice α] [bounded_order α] [is_modular_lattice α] {a b c : α}
+  [lattice α] [order_bot α] [is_modular_lattice α] {a b c : α}
   (h : disjoint b c) (hsup : disjoint a (b ⊔ c)) :
   disjoint (a ⊔ b) c :=
 begin

src/order/order_iso_nat.lean

@@ -176,12 +176,12 @@ end
 type, `monotonic_sequence_limit_index a` is the least natural number `n` for which `aₙ` reaches the
 constant value. For sequences that are not eventually constant, `monotonic_sequence_limit_index a`
 is defined, but is a junk value. -/
-noncomputable def monotonic_sequence_limit_index {α : Type*} [partial_order α] (a : ℕ →o α) : ℕ :=
+noncomputable def monotonic_sequence_limit_index {α : Type*} [preorder α] (a : ℕ →o α) : ℕ :=
 Inf { n | ∀ m, n ≤ m → a n = a m }
 
 /-- The constant value of an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a
 partially-ordered type. -/
-noncomputable def monotonic_sequence_limit {α : Type*} [partial_order α] (a : ℕ →o α) :=
+noncomputable def monotonic_sequence_limit {α : Type*} [preorder α] (a : ℕ →o α) :=
 a (monotonic_sequence_limit_index a)
 
 lemma well_founded.supr_eq_monotonic_sequence_limit {α : Type*} [complete_lattice α]