refactor(*): split order_{top,bot} from lattice hierarchy (#9891)

Rename `bounded_lattice` to `bounded_order`.
Split out `order_{top,bot}` and `bounded_order` from the order hierarchy.
That means that we no longer have `semilattice_{sup,inf}_{top,bot}`, but use the `[order_top]` as a mixin to `semilattice_inf`, for example.
Similarly, `lattice` and `bounded_order` instead of what was before `bounded_lattice`.
Similarly, `distrib_lattice` and `bounded_order` instead of what was before `bounded_distrib_lattice`.

scripts/nolints.txt

@@ -218,7 +218,7 @@ apply_nolint list.traverse doc_blame
 apply_nolint multiset.traverse doc_blame
 
 -- data/nat/basic.lean
-apply_nolint nat.subtype.semilattice_sup_bot fails_quickly
+apply_nolint nat.subtype.order_bot fails_quickly
 
 -- data/num/bitwise.lean
 apply_nolint snum.cadd doc_blame
@@ -994,4 +994,4 @@ apply_nolint Cauchy.gen doc_blame
 apply_nolint uniform_space.completion.completion_separation_quotient_equiv doc_blame
 apply_nolint uniform_space.completion.cpkg doc_blame
 apply_nolint uniform_space.completion.extension₂ doc_blame
-apply_nolint uniform_space.completion.map₂ doc_blame
+apply_nolint uniform_space.completion.map₂ doc_blame

src/algebra/associated.lean

@@ -603,6 +603,10 @@ instance : order_top (associates α) :=
 { top := 0,
   le_top := assume a, ⟨0, (mul_zero a).symm⟩ }
 
+instance : bounded_order (associates α) :=
+{ .. associates.order_top,
+  .. associates.order_bot }
+
 instance [nontrivial α] : nontrivial (associates α) :=
 ⟨⟨0, 1,
 assume h,

src/algebra/big_operators/basic.lean

@@ -276,12 +276,12 @@ For a version expressed with subtypes, see `fintype.prod_subtype_mul_prod_subtyp
 For a version expressed with subtypes, see `fintype.sum_subtype_add_sum_subtype`. "]
 lemma prod_mul_prod_compl [fintype α] [decidable_eq α] (s : finset α) (f : α → β) :
   (∏ i in s, f i) * (∏ i in sᶜ, f i) = ∏ i, f i :=
-is_compl_compl.prod_mul_prod f
+is_compl.prod_mul_prod is_compl_compl f
 
 @[to_additive]
 lemma prod_compl_mul_prod [fintype α] [decidable_eq α] (s : finset α) (f : α → β) :
   (∏ i in sᶜ, f i) * (∏ i in s, f i) = ∏ i, f i :=
-is_compl_compl.symm.prod_mul_prod f
+(@is_compl_compl _ s _).symm.prod_mul_prod f
 
 @[to_additive]
 lemma prod_sdiff [decidable_eq α] (h : s₁ ⊆ s₂) :

src/algebra/order/monoid.lean

@@ -7,7 +7,7 @@ import algebra.group.with_one
 import algebra.group.type_tags
 import algebra.group.prod
 import algebra.order.monoid_lemmas
-import order.bounded_lattice
+import order.bounded_order
 import order.min_max
 import order.rel_iso
 
@@ -629,8 +629,8 @@ section canonically_linear_ordered_monoid
 variables [canonically_linear_ordered_monoid α]
 
 @[priority 100, to_additive]  -- see Note [lower instance priority]
-instance canonically_linear_ordered_monoid.semilattice_sup_bot : semilattice_sup_bot α :=
-{ ..lattice_of_linear_order, ..canonically_ordered_monoid.to_order_bot α }
+instance canonically_linear_ordered_monoid.semilattice_sup : semilattice_sup α :=
+{ ..lattice_of_linear_order }
 
 instance with_top.canonically_linear_ordered_add_monoid
   (α : Type*) [canonically_linear_ordered_add_monoid α] :

src/algebra/order/nonneg.lean

@@ -52,16 +52,20 @@ lemma bot_eq [preorder α] {a : α} : (⊥ : {x : α // a ≤ x}) = ⟨a, le_rfl
 instance no_top_order [partial_order α] [no_top_order α] {a : α} : no_top_order {x : α // a ≤ x} :=
 set.Ici.no_top_order
 
-/-- This instance uses data fields from `subtype.partial_order` to help type-class inference.
-The `set.Ici` data fields are definitionally equal, but that requires unfolding semireducible
-definitions, so type-class inference won't see this. -/
-instance semilattice_inf_bot [semilattice_inf α] {a : α} : semilattice_inf_bot {x : α // a ≤ x} :=
-{ ..nonneg.order_bot, ..set.Ici.semilattice_inf_bot }
+instance semilattice_inf [semilattice_inf α] {a : α} : semilattice_inf {x : α // a ≤ x} :=
+set.Ici.semilattice_inf
 
 instance densely_ordered [preorder α] [densely_ordered α] {a : α} :
   densely_ordered {x : α // a ≤ x} :=
 show densely_ordered (Ici a), from set.densely_ordered
 
+/-- If `Sup ∅ ≤ a` then `{x : α // a ≤ x}` is a `conditionally_complete_linear_order`. -/
+@[reducible]
+protected noncomputable def conditionally_complete_linear_order
+  [conditionally_complete_linear_order α] {a : α} :
+  conditionally_complete_linear_order {x : α // a ≤ x} :=
+{ .. @ord_connected_subset_conditionally_complete_linear_order α (set.Ici a) _ ⟨⟨a, le_rfl⟩⟩ _ }
+
 /-- If `Sup ∅ ≤ a` then `{x : α // a ≤ x}` is a `conditionally_complete_linear_order_bot`.
 
 This instance uses data fields from `subtype.linear_order` to help type-class inference.
@@ -75,8 +79,7 @@ protected noncomputable def conditionally_complete_linear_order_bot
     (@subset_Sup_def α (set.Ici a) _ ⟨⟨a, le_rfl⟩⟩) ∅).trans $ subtype.eq $
       by { rw bot_eq, cases h.lt_or_eq with h2 h2, { simp [h2.not_le] }, simp [h2] },
   ..nonneg.order_bot,
-  ..(by apply_instance : linear_order {x : α // a ≤ x}),
-  .. @ord_connected_subset_conditionally_complete_linear_order α (set.Ici a) _ ⟨⟨a, le_rfl⟩⟩ _ }
+  ..nonneg.conditionally_complete_linear_order }
 
 instance inhabited [preorder α] {a : α} : inhabited {x : α // a ≤ x} :=
 ⟨⟨a, le_rfl⟩⟩

src/algebra/tropical/basic.lean

@@ -109,6 +109,7 @@ def trop_rec {F : Π (X : tropical R), Sort v} (h : Π X, F (trop X)) : Π X, F
 
 section order
 
+-- TODO: generalize this to a `has_le` and use below in `le_zero` and `order_top`
 instance [preorder R] : preorder (tropical R) :=
 { le := λ x y, untrop x ≤ untrop y,
   le_refl := λ _, le_refl _,
@@ -146,7 +147,6 @@ instance [has_top R] : has_top (tropical R) := ⟨0⟩
 
 instance [partial_order R] : order_top (tropical (with_top R)) :=
 { le_top := λ a a' h, option.no_confusion h,
-  ..tropical.partial_order,
   ..tropical.has_top }
 
 variable [linear_order R]

src/analysis/box_integral/box/basic.lean

@@ -32,7 +32,7 @@ We define the following operations on boxes:
 * coercion to `set (ι → ℝ)` and `has_mem (ι → ℝ) (box_integral.box ι)` as described above;
 * `partial_order` and `semilattice_sup` instances such that `I ≤ J` is equivalent to
   `(I : set (ι → ℝ)) ⊆ J`;
-* `lattice` and `semilattice_inf_bot` instances on `with_bot (box_integral.box ι)`;
+* `lattice` instances on `with_bot (box_integral.box ι)`;
 * `box_integral.box.Icc`: the closed box `set.Icc I.lower I.upper`; defined as a bundled monotone
   map from `box ι` to `set (ι → ℝ)`;
 * `box_integral.box.face I i : box (fin n)`: a hyperface of `I : box_integral.box (fin (n + 1))`;
@@ -269,9 +269,6 @@ instance : lattice (with_bot (box ι)) :=
     end,
   .. with_bot.semilattice_sup, .. box.with_bot.has_inf }
 
-instance : semilattice_inf_bot (with_bot (box ι)) :=
-{ .. box.with_bot.lattice, .. with_bot.semilattice_sup }
-
 @[simp, norm_cast] lemma disjoint_with_bot_coe {I J : with_bot (box ι)} :
   disjoint (I : set (ι → ℝ)) J ↔ disjoint I J :=
 by { simp only [disjoint, ← with_bot_coe_subset_iff, coe_inf], refl }

src/analysis/box_integral/partition/basic.lean

@@ -26,7 +26,7 @@ boxes of `π` actually cover the whole `I`. We also define some operations on pr
 * `box_integral.partition.bUnion`: split each box of a partition into smaller boxes;
 * `box_integral.partition.restrict`: restrict a partition to a smaller box.
 
-We also define a `semilattice_inf_top` structure on `box_integral.partition I` for all
+We also define a `semilattice_inf` structure on `box_integral.partition I` for all
 `I : box_integral.box ι`.
 
 ## Tags
@@ -478,14 +478,12 @@ by simp only [inf_def, mem_bUnion, mem_restrict]
 @[simp] lemma Union_inf (π₁ π₂ : prepartition I) : (π₁ ⊓ π₂).Union = π₁.Union ∩ π₂.Union :=
 by simp only [inf_def, Union_bUnion, Union_restrict, ← Union_inter, ← Union_def]
 
-instance : semilattice_inf_top (prepartition I) :=
+instance : semilattice_inf (prepartition I) :=
 { inf_le_left := λ π₁ π₂, π₁.bUnion_le _,
   inf_le_right := λ π₁ π₂, (bUnion_le_iff _).2 (λ J hJ, le_rfl),
   le_inf := λ π π₁ π₂ h₁ h₂, π₁.le_bUnion_iff.2 ⟨h₁, λ J hJ, restrict_mono h₂⟩,
-  ..prepartition.partial_order, .. prepartition.order_top, .. prepartition.has_inf }
-
-instance : semilattice_inf_bot (prepartition I) :=
-{ .. prepartition.order_bot, .. prepartition.semilattice_inf_top }
+  .. prepartition.has_inf,
+  .. prepartition.partial_order }
 
 /-- The prepartition with boxes `{J ∈ π | p J}`. -/
 @[simps] def filter (π : prepartition I) (p : box ι → Prop) : prepartition I :=

src/analysis/box_integral/partition/filter.lean

@@ -23,7 +23,7 @@ assumptions.
 Finally, for each set of parameters `l : box_integral.integration_params` and a rectangular box
 `I : box_integral.box ι`, we define several `filter`s that will be used either in the definition of
 the corresponding integral, or in the proofs of its properties. We equip
-`box_integral.integration_params` with a `bounded_lattice` structure such that larger
+`box_integral.integration_params` with a `bounded_order` structure such that larger
 `integration_params` produce larger filters.
 
 ## Main definitions
@@ -202,12 +202,12 @@ def equiv_prod : integration_params ≃ bool × order_dual bool × order_dual bo
 instance : partial_order integration_params :=
 partial_order.lift equiv_prod equiv_prod.injective
 
-/-- Auxiliary `order_iso` with a product type used to lift a `bounded_lattice` structure. -/
+/-- Auxiliary `order_iso` with a product type used to lift a `bounded_order` structure. -/
 def iso_prod : integration_params ≃o bool × order_dual bool × order_dual bool :=
 ⟨equiv_prod, λ ⟨x, y, z⟩, iff.rfl⟩
 
-instance : bounded_lattice integration_params :=
-iso_prod.symm.to_galois_insertion.lift_bounded_lattice
+instance : bounded_order integration_params :=
+iso_prod.symm.to_galois_insertion.lift_bounded_order
 
 /-- The value `⊥` (`bRiemann = ff`, `bHenstock = tt`, `bDistortion = tt`) corresponds to a
 generalization of the Henstock integral such that the Divergence theorem holds true without

src/analysis/normed_space/enorm.lean

@@ -126,7 +126,7 @@ noncomputable instance : order_top (enorm 𝕜 V) :=
 { top := ⊤,
   le_top := λ e x, if h : x = 0 then by simp [h] else by simp [top_map h] }
 
-noncomputable instance : semilattice_sup_top (enorm 𝕜 V) :=
+noncomputable instance : semilattice_sup (enorm 𝕜 V) :=
 { le := (≤),
   lt := (<),
   sup := λ e₁ e₂,
@@ -139,7 +139,6 @@ noncomputable instance : semilattice_sup_top (enorm 𝕜 V) :=
   le_sup_left := λ e₁ e₂ x, le_max_left _ _,
   le_sup_right := λ e₁ e₂ x, le_max_right _ _,
   sup_le := λ e₁ e₂ e₃ h₁ h₂ x, max_le (h₁ x) (h₂ x),
-  .. enorm.order_top,
   .. enorm.partial_order }
 
 @[simp, norm_cast] lemma coe_max (e₁ e₂ : enorm 𝕜 V) : ⇑(e₁ ⊔ e₂) = λ x, max (e₁ x) (e₂ x) := rfl

src/category_theory/filtered.lean

@@ -7,7 +7,7 @@ import category_theory.fin_category
 import category_theory.limits.cones
 import category_theory.adjunction.basic
 import category_theory.category.preorder
-import order.bounded_lattice
+import order.bounded_order
 
 /-!
 # Filtered categories
@@ -100,8 +100,8 @@ instance is_filtered_of_directed_order_nonempty
   (α : Type u) [directed_order α] [nonempty α] : is_filtered α := {}
 
 -- Sanity checks
-example (α : Type u) [semilattice_sup_bot α] : is_filtered α := by apply_instance
-example (α : Type u) [semilattice_sup_top α] : is_filtered α := by apply_instance
+example (α : Type u) [semilattice_sup α] [order_bot α] : is_filtered α := by apply_instance
+example (α : Type u) [semilattice_sup α] [order_top α] : is_filtered α := by apply_instance
 
 namespace is_filtered
 
@@ -473,8 +473,8 @@ instance is_cofiltered_of_semilattice_inf_nonempty
   (α : Type u) [semilattice_inf α] [nonempty α] : is_cofiltered α := {}
 
 -- Sanity checks
-example (α : Type u) [semilattice_inf_bot α] : is_cofiltered α := by apply_instance
-example (α : Type u) [semilattice_inf_top α] : is_cofiltered α := by apply_instance
+example (α : Type u) [semilattice_inf α] [order_bot α] : is_cofiltered α := by apply_instance
+example (α : Type u) [semilattice_inf α] [order_top α] : is_cofiltered α := by apply_instance
 
 namespace is_cofiltered
 

src/category_theory/limits/lattice.lean

@@ -27,92 +27,96 @@ variables {α : Type u}
 variables {J : Type u} [small_category J] [fin_category J]
 
 /--
-The limit cone over any functor from a finite diagram into a `semilattice_inf_top`.
+The limit cone over any functor from a finite diagram into a `semilattice_inf` with `order_top`.
 -/
-def finite_limit_cone [semilattice_inf_top α] (F : J ⥤ α) : limit_cone F :=
+def finite_limit_cone [semilattice_inf α] [order_top α] (F : J ⥤ α) : limit_cone F :=
 { cone :=
   { X := finset.univ.inf F.obj,
     π := { app := λ j, hom_of_le (finset.inf_le (fintype.complete _)) } },
   is_limit := { lift := λ s, hom_of_le (finset.le_inf (λ j _, (s.π.app j).down.down)) } }
 
 /--
-The colimit cocone over any functor from a finite diagram into a `semilattice_sup_bot`.
+The colimit cocone over any functor from a finite diagram into a `semilattice_sup` with `order_bot`.
 -/
-def finite_colimit_cocone [semilattice_sup_bot α] (F : J ⥤ α) : colimit_cocone F :=
+def finite_colimit_cocone [semilattice_sup α] [order_bot α] (F : J ⥤ α) : colimit_cocone F :=
 { cocone :=
   { X := finset.univ.sup F.obj,
     ι := { app := λ i, hom_of_le (finset.le_sup (fintype.complete _)) } },
   is_colimit := { desc := λ s, hom_of_le (finset.sup_le (λ j _, (s.ι.app j).down.down)) } }
 
 @[priority 100] -- see Note [lower instance priority]
-instance has_finite_limits_of_semilattice_inf_top [semilattice_inf_top α] :
+instance has_finite_limits_of_semilattice_inf_order_top [semilattice_inf α] [order_top α] :
   has_finite_limits α :=
 ⟨λ J 𝒥₁ 𝒥₂, by exactI { has_limit := λ F, has_limit.mk (finite_limit_cone F) }⟩
 
 @[priority 100] -- see Note [lower instance priority]
-instance has_finite_colimits_of_semilattice_sup_bot [semilattice_sup_bot α] :
+instance has_finite_colimits_of_semilattice_sup_order_bot [semilattice_sup α] [order_bot α] :
   has_finite_colimits α :=
 ⟨λ J 𝒥₁ 𝒥₂, by exactI { has_colimit := λ F, has_colimit.mk (finite_colimit_cocone F) }⟩
 
 /--
-The limit of a functor from a finite diagram into a `semilattice_inf_top` is the infimum of the
-objects in the image.
+The limit of a functor from a finite diagram into a `semilattice_inf` with `order_top` is the
+infimum of the objects in the image.
 -/
-lemma finite_limit_eq_finset_univ_inf [semilattice_inf_top α] (F : J ⥤ α) :
+lemma finite_limit_eq_finset_univ_inf [semilattice_inf α] [order_top α] (F : J ⥤ α) :
   limit F = finset.univ.inf F.obj :=
 (is_limit.cone_point_unique_up_to_iso (limit.is_limit F)
   (finite_limit_cone F).is_limit).to_eq
 
 /--
-The colimit of a functor from a finite diagram into a `semilattice_sup_bot` is the supremum of the
-objects in the image.
+The colimit of a functor from a finite diagram into a `semilattice_sup` with `order_bot`
+is the supremum of the objects in the image.
 -/
-lemma finite_colimit_eq_finset_univ_sup [semilattice_sup_bot α] (F : J ⥤ α) :
+lemma finite_colimit_eq_finset_univ_sup [semilattice_sup α] [order_bot α] (F : J ⥤ α) :
   colimit F = finset.univ.sup F.obj :=
 (is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit F)
   (finite_colimit_cocone F).is_colimit).to_eq
 
 /--
-A finite product in the category of a `semilattice_inf_top` is the same as the infimum.
+A finite product in the category of a `semilattice_inf` with `order_top` is the same as the infimum.
 -/
-lemma finite_product_eq_finset_inf [semilattice_inf_top α] {ι : Type u} [decidable_eq ι]
+lemma finite_product_eq_finset_inf [semilattice_inf α] [order_top α] {ι : Type u} [decidable_eq ι]
   [fintype ι] (f : ι → α) : (∏ f) = (fintype.elems ι).inf f :=
 (is_limit.cone_point_unique_up_to_iso (limit.is_limit _)
   (finite_limit_cone (discrete.functor f)).is_limit).to_eq
 
 /--
-A finite coproduct in the category of a `semilattice_sup_bot` is the same as the supremum.
+A finite coproduct in the category of a `semilattice_sup` with `order_bot` is the same as the
+supremum.
 -/
-lemma finite_coproduct_eq_finset_sup [semilattice_sup_bot α] {ι : Type u} [decidable_eq ι]
+lemma finite_coproduct_eq_finset_sup [semilattice_sup α] [order_bot α] {ι : Type u} [decidable_eq ι]
   [fintype ι] (f : ι → α) : (∐ f) = (fintype.elems ι).sup f :=
 (is_colimit.cocone_point_unique_up_to_iso (colimit.is_colimit _)
   (finite_colimit_cocone (discrete.functor f)).is_colimit).to_eq
 
 /--
-The binary product in the category of a `semilattice_inf_top` is the same as the infimum.
+The binary product in the category of a `semilattice_inf` with `order_top` is the same as the
+infimum.
 -/
 @[simp]
-lemma prod_eq_inf [semilattice_inf_top α] (x y : α) : limits.prod x y = x ⊓ y :=
+lemma prod_eq_inf [semilattice_inf α] [order_top α] (x y : α) : limits.prod x y = x ⊓ y :=
 calc limits.prod x y = limit (pair x y) : rfl
 ... = finset.univ.inf (pair x y).obj : by rw finite_limit_eq_finset_univ_inf (pair x y)
 ... = x ⊓ (y ⊓ ⊤) : rfl -- Note: finset.inf is realized as a fold, hence the definitional equality
 ... = x ⊓ y : by rw inf_top_eq
 
 /--
-The binary coproduct in the category of a `semilattice_sup_bot` is the same as the supremum.
+The binary coproduct in the category of a `semilattice_sup` with `order_bot` is the same as the
+supremum.
 -/
 @[simp]
-lemma coprod_eq_sup [semilattice_sup_bot α] (x y : α) : limits.coprod x y = x ⊔ y :=
+lemma coprod_eq_sup [semilattice_sup α] [order_bot α] (x y : α) : limits.coprod x y = x ⊔ y :=
 calc limits.coprod x y = colimit (pair x y) : rfl
 ... = finset.univ.sup (pair x y).obj : by rw finite_colimit_eq_finset_univ_sup (pair x y)
 ... = x ⊔ (y ⊔ ⊥) : rfl -- Note: finset.sup is realized as a fold, hence the definitional equality
 ... = x ⊔ y : by rw sup_bot_eq
 
 /--
-The pullback in the category of a `semilattice_inf_top` is the same as the infimum over the objects.
+The pullback in the category of a `semilattice_inf` with `order_top` is the same as the infimum
+over the objects.
 -/
 @[simp]
-lemma pullback_eq_inf [semilattice_inf_top α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z) :
+lemma pullback_eq_inf [semilattice_inf α] [order_top α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z) :
   pullback f g = x ⊓ y :=
 calc pullback f g = limit (cospan f g) : rfl
 ... = finset.univ.inf (cospan f g).obj : by rw finite_limit_eq_finset_univ_inf
@@ -121,10 +125,11 @@ calc pullback f g = limit (cospan f g) : rfl
 ... = x ⊓ y : inf_eq_right.mpr (inf_le_of_left_le f.le)
 
 /--
-The pushout in the category of a `semilattice_sup_bot` is the same as the supremum over the objects.
+The pushout in the category of a `semilattice_sup` with `order_bot` is the same as the supremum
+over the objects.
 -/
 @[simp]
-lemma pushout_eq_sup [semilattice_sup_bot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y) :
+lemma pushout_eq_sup [semilattice_sup α] [order_bot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y) :
   pushout f g = x ⊔ y :=
 calc pushout f g = colimit (span f g) : rfl
 ... = finset.univ.sup (span f g).obj : by rw finite_colimit_eq_finset_univ_sup