refactor(order): order_{top,bot} as mixin (#10097)

This changes `order_top α` / `order_bot α` to _require_ `has_le α` instead of _extending_ `partial_order α`.
As a result, `order_top` can be combined with other lattice typeclasses. This lends itself to more refactors downstream, such as phrasing lemmas that currently require orders/semilattices and top/bot to provide them as separate TC inference, instead of "bundled" classes like `semilattice_inf_top`.

This refactor also provides the basis for making more consistent the "extended" algebraic classes, like "e(nn)real", "enat", etc. Some proof terms for lemmas about `nnreal` and `ennreal` have been switched to rely on more direct coercions from the underlying non-extended type or other (semi)rings.

Modify `semilattice_{inf,sup}_{top,bot}` to not directly inherit from
`order_{top,bot}`. Instead, they are now extending from `has_{top,bot}`. Extending `order_{top,bot}` is now only possible is `has_le` is provided to the TC cache at `extends` declaration time, when using `old_structure_cmd true`. That is,
```
set_option old_structure_cmd true

class mnwe (α : Type u) extends semilattice_inf α, order_top α.
```
errors with
```
type mismatch at application
  @semilattice_inf.to_partial_order α top
term
  top
has type
  α
but is expected to have type
  semilattice_inf α
```
One can make this work through one of three ways:
No `old_structure_cmd`, which is unfriendly to the rest of the class hierarchy
Require `has_le` in `class mwe (α : Type u) [has_le α] extends semilattice_inf α, order_top α.`, which is unfriendly to the existing hierarchy and how lemmas are stated.
Provide an additional axiom on top of a "data-only" TC and have a low-priority instance:
```
class semilattice_inf_top (α : Type u) extends semilattice_inf α, has_top α :=
(le_top : ∀ a : α, a ≤ ⊤)

@[priority 100]
instance semilattice_inf_top.to_order_top : order_top α :=
{ top := ⊤,  le_top := semilattice_inf_top.le_top }
```
The third option is chosen in this refactor.

Pulled out from #9891, without the semilattice refactor.



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

src/algebra/associated.lean

@@ -573,6 +573,10 @@ theorem le_mul_right {a b : associates α} : a ≤ a * b := ⟨b, rfl⟩
 theorem le_mul_left {a b : associates α} : a ≤ b * a :=
 by rw [mul_comm]; exact le_mul_right
 
+instance : order_bot (associates α) :=
+{ bot := 1,
+  bot_le := assume a, one_le }
+
 end order
 
 end comm_monoid
@@ -595,6 +599,10 @@ instance : comm_monoid_with_zero (associates α) :=
   mul_zero := by { rintro ⟨a⟩, show associates.mk (a * 0) = associates.mk 0, rw [mul_zero] },
   .. associates.comm_monoid, .. associates.has_zero }
 
+instance : order_top (associates α) :=
+{ top := 0,
+  le_top := assume a, ⟨0, (mul_zero a).symm⟩ }
+
 instance [nontrivial α] : nontrivial (associates α) :=
 ⟨⟨0, 1,
 assume h,
@@ -711,16 +719,6 @@ instance : partial_order (associates α) :=
   quot.sound $ associated_of_dvd_dvd (dvd_of_mk_le_mk hab) (dvd_of_mk_le_mk hba))
   .. associates.preorder }
 
-instance : order_bot (associates α) :=
-{ bot := 1,
-  bot_le := assume a, one_le,
-  .. associates.partial_order }
-
-instance : order_top (associates α) :=
-{ top := 0,
-  le_top := assume a, ⟨0, (mul_zero a).symm⟩,
-  .. associates.partial_order }
-
 instance : no_zero_divisors (associates α) :=
 ⟨λ x y,
   (quotient.induction_on₂ x y $ assume a b h,

src/algebra/module/submodule_lattice.lean

@@ -53,8 +53,7 @@ instance unique_bot : unique (⊥ : submodule R M) :=
 
 instance : order_bot (submodule R M) :=
 { bot := ⊥,
-  bot_le := λ p x, by simp {contextual := tt},
-  ..set_like.partial_order }
+  bot_le := λ p x, by simp {contextual := tt} }
 
 protected lemma eq_bot_iff (p : submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x = (0 : M) :=
 ⟨ λ h, h.symm ▸ λ x hx, (mem_bot R).mp hx,
@@ -109,8 +108,7 @@ end
 
 instance : order_top (submodule R M) :=
 { top := ⊤,
-  le_top := λ p x _, trivial,
-  ..set_like.partial_order }
+  le_top := λ p x _, trivial }
 
 lemma eq_top_iff' {p : submodule R M} : p = ⊤ ↔ ∀ x, x ∈ p :=
 eq_top_iff.trans ⟨λ h x, h trivial, λ h x _, h x⟩
@@ -160,7 +158,8 @@ instance : complete_lattice (submodule R M) :=
   le_Inf       := λ s a, le_Inf',
   Inf_le       := λ s a, Inf_le',
   ..submodule.order_top,
-  ..submodule.order_bot }
+  ..submodule.order_bot,
+  ..set_like.partial_order }
 
 @[simp] theorem inf_coe : ↑(p ⊓ q) = (p ∩ q : set M) := rfl
 

src/algebra/order/monoid.lean

@@ -96,11 +96,17 @@ class linear_ordered_comm_monoid_with_zero (α : Type*)
 
 /-- A linearly ordered commutative monoid with an additively absorbing `⊤` element.
   Instances should include number systems with an infinite element adjoined.` -/
-@[protect_proj, ancestor linear_ordered_add_comm_monoid order_top]
+@[protect_proj, ancestor linear_ordered_add_comm_monoid has_top]
 class linear_ordered_add_comm_monoid_with_top (α : Type*)
-  extends linear_ordered_add_comm_monoid α, order_top α :=
+  extends linear_ordered_add_comm_monoid α, has_top α :=
+(le_top : ∀ x : α, x ≤ ⊤)
 (top_add' : ∀ x : α, ⊤ + x = ⊤)
 
+@[priority 100]    -- see Note [lower instance priority]
+instance linear_ordered_add_comm_monoid_with_top.to_order_top (α : Type u)
+  [h : linear_ordered_add_comm_monoid_with_top α] : order_top α :=
+{ ..h }
+
 section linear_ordered_add_comm_monoid_with_top
 variables [linear_ordered_add_comm_monoid_with_top α] {a b : α}
 
@@ -460,10 +466,16 @@ end with_bot
   which is to say, `a ≤ b` iff there exists `c` with `b = a + c`.
   This is satisfied by the natural numbers, for example, but not
   the integers or other nontrivial `ordered_add_comm_group`s. -/
-@[protect_proj, ancestor ordered_add_comm_monoid order_bot]
-class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoid α, order_bot α :=
+@[protect_proj, ancestor ordered_add_comm_monoid has_bot]
+class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoid α, has_bot α :=
+(bot_le : ∀ x : α, ⊥ ≤ x)
 (le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)
 
+@[priority 100]  -- see Note [lower instance priority]
+instance canonically_ordered_add_monoid.to_order_bot (α : Type u)
+  [h : canonically_ordered_add_monoid α] : order_bot α :=
+{ ..h }
+
 /-- A canonically ordered monoid is an ordered commutative monoid
   in which the ordering coincides with the divisibility relation,
   which is to say, `a ≤ b` iff there exists `c` with `b = a * c`.
@@ -473,10 +485,16 @@ class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoi
   Dedekind domain satisfy this; collections of all things ≤ 1 seem to
   be more natural that collections of all things ≥ 1).
 -/
-@[protect_proj, ancestor ordered_comm_monoid order_bot, to_additive]
-class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α, order_bot α :=
+@[protect_proj, ancestor ordered_comm_monoid has_bot, to_additive]
+class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α, has_bot α :=
+(bot_le : ∀ x : α, ⊥ ≤ x)
 (le_iff_exists_mul : ∀ a b : α, a ≤ b ↔ ∃ c, b = a * c)
 
+@[priority 100, to_additive]  -- see Note [lower instance priority]
+instance canonically_ordered_monoid.to_order_bot (α : Type u)
+  [h : canonically_ordered_monoid α] : order_bot α :=
+{ ..h }
+
 section canonically_ordered_monoid
 
 variables [canonically_ordered_monoid α] {a b c d : α}

src/algebra/order/nonneg.lean

@@ -44,8 +44,10 @@ namespace nonneg
 /-- 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 order_bot [partial_order α] {a : α} : order_bot {x : α // a ≤ x} :=
-{ ..subtype.partial_order _, ..set.Ici.order_bot }
+instance order_bot [preorder α] {a : α} : order_bot {x : α // a ≤ x} :=
+{ ..set.Ici.order_bot }
+
+lemma bot_eq [preorder α] {a : α} : (⊥ : {x : α // a ≤ x}) = ⟨a, le_rfl⟩ := rfl
 
 instance no_top_order [partial_order α] [no_top_order α] {a : α} : no_top_order {x : α // a ≤ x} :=
 set.Ici.no_top_order
@@ -71,7 +73,7 @@ protected noncomputable def conditionally_complete_linear_order_bot
   conditionally_complete_linear_order_bot {x : α // a ≤ x} :=
 { cSup_empty := (function.funext_iff.1
     (@subset_Sup_def α (set.Ici a) _ ⟨⟨a, le_rfl⟩⟩) ∅).trans $ subtype.eq $
-      by { cases h.lt_or_eq with h2 h2, { simp [h2.not_le] }, simp [h2] },
+      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⟩⟩ _ }

src/algebra/tropical/basic.lean

@@ -141,7 +141,8 @@ instance [has_top R] : has_top (tropical R) := ⟨0⟩
 @[simp] lemma trop_coe_ne_zero (x : R) : trop (x : with_top R) ≠ 0 .
 @[simp] lemma zero_ne_trop_coe (x : R) : (0 : tropical (with_top R)) ≠ trop x .
 
-@[simp] lemma le_zero [order_top R] (x : tropical R) : x ≤ 0 := le_top
+-- TODO: generalize to `has_le`
+@[simp] lemma le_zero [preorder R] [order_top R] (x : tropical R) : x ≤ 0 := le_top
 
 instance [partial_order R] : order_top (tropical (with_top R)) :=
 { le_top := λ a a' h, option.no_confusion h,

src/analysis/box_integral/partition/basic.lean

@@ -93,7 +93,7 @@ by { rintro ⟨s₁, h₁, h₁'⟩ ⟨s₂, h₂, h₂'⟩ (rfl : s₁ = s₂),
 /-- We say that `π ≤ π'` if each box of `π` is a subbox of some box of `π'`. -/
 instance : has_le (prepartition I) := ⟨λ π π', ∀ ⦃I⦄, I ∈ π → ∃ I' ∈ π', I ≤ I'⟩
 
-instance : order_top (prepartition I) :=
+instance : partial_order (prepartition I) :=
 { le := (≤),
   le_refl := λ π I hI, ⟨I, hI, le_rfl⟩,
   le_trans := λ π₁ π₂ π₃ h₁₂ h₂₃ I₁ hI₁,
@@ -107,14 +107,15 @@ instance : order_top (prepartition I) :=
       obtain rfl : J = J'', from π₁.eq_of_le hJ hJ'' (hle.trans hle'),
       obtain rfl : J' = J, from le_antisymm ‹_› ‹_›,
       assumption
-    end,
-  top := single I I le_rfl,
+    end }
+
+instance : order_top (prepartition I) :=
+{ top := single I I le_rfl,
   le_top := λ π J hJ, ⟨I, by simp, π.le_of_mem hJ⟩ }
 
 instance : order_bot (prepartition I) :=
 { bot := ⟨∅, λ J hJ, false.elim hJ, λ J hJ, false.elim hJ⟩,
-  bot_le := λ π J hJ, false.elim hJ,
-  .. prepartition.order_top }
+  bot_le := λ π J hJ, false.elim hJ }
 
 instance : inhabited (prepartition I) := ⟨⊤⟩
 
@@ -481,7 +482,7 @@ instance : semilattice_inf_top (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.order_top, .. prepartition.has_inf }
+  ..prepartition.partial_order, .. prepartition.order_top, .. prepartition.has_inf }
 
 instance : semilattice_inf_bot (prepartition I) :=
 { .. prepartition.order_bot, .. prepartition.semilattice_inf_top }

src/analysis/convex/cone.lean

@@ -452,7 +452,8 @@ lemma step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x)
   (dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s) (hdom : f.domain ≠ ⊤) :
   ∃ g, f < g ∧ ∀ x : g.domain, (x : E) ∈ s → 0 ≤ g x :=
 begin
-  rcases set_like.exists_of_lt (lt_top_iff_ne_top.2 hdom) with ⟨y, hy', hy⟩, clear hy',
+  obtain ⟨y, -, hy⟩ : ∃ (y : E) (h : y ∈ ⊤), y ∉ f.domain,
+    { exact @set_like.exists_of_lt (submodule ℝ E) _ _ _ _ (lt_top_iff_ne_top.2 hdom) },
   obtain ⟨c, le_c, c_le⟩ :
     ∃ c, (∀ x : f.domain, -(x:E) - y ∈ s → f x ≤ c) ∧ (∀ x : f.domain, (x:E) + y ∈ s → c ≤ f x),
   { set Sp := f '' {x : f.domain | (x:E) + y ∈ s},

src/analysis/normed/group/basic.lean

@@ -546,13 +546,13 @@ lemma nndist_eq_nnnorm (a b : E) : nndist a b = ∥a - b∥₊ := nnreal.eq $ di
 nnreal.eq norm_zero
 
 lemma nnnorm_add_le (g h : E) : ∥g + h∥₊ ≤ ∥g∥₊ + ∥h∥₊ :=
-nnreal.coe_le_coe.2 $ norm_add_le g h
+nnreal.coe_le_coe.1 $ norm_add_le g h
 
 @[simp] lemma nnnorm_neg (g : E) : ∥-g∥₊ = ∥g∥₊ :=
 nnreal.eq $ norm_neg g
 
 lemma nndist_nnnorm_nnnorm_le (g h : E) : nndist ∥g∥₊ ∥h∥₊ ≤ ∥g - h∥₊ :=
-nnreal.coe_le_coe.2 $ dist_norm_norm_le g h
+nnreal.coe_le_coe.1 $ dist_norm_norm_le g h
 
 lemma of_real_norm_eq_coe_nnnorm (x : E) : ennreal.of_real ∥x∥ = (∥x∥₊ : ℝ≥0∞) :=
 ennreal.of_real_eq_coe_nnreal _
@@ -568,7 +568,7 @@ by rw [emetric.mem_ball, edist_eq_coe_nnnorm]
 
 lemma nndist_add_add_le (g₁ g₂ h₁ h₂ : E) :
   nndist (g₁ + g₂) (h₁ + h₂) ≤ nndist g₁ h₁ + nndist g₂ h₂ :=
-nnreal.coe_le_coe.2 $ dist_add_add_le g₁ g₂ h₁ h₂
+nnreal.coe_le_coe.1 $ dist_add_add_le g₁ g₂ h₁ h₂
 
 lemma edist_add_add_le (g₁ g₂ h₁ h₂ : E) :
   edist (g₁ + g₂) (h₁ + h₂) ≤ edist g₁ h₁ + edist g₂ h₂ :=

src/analysis/normed_space/enorm.lean

@@ -122,11 +122,13 @@ noncomputable instance : inhabited (enorm 𝕜 V) := ⟨⊤⟩
 
 lemma top_map {x : V} (hx : x ≠ 0) : (⊤ : enorm 𝕜 V) x = ⊤ := if_neg hx
 
+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) :=
 { le := (≤),
   lt := (<),
-  top := ⊤,
-  le_top := λ e x, if h : x = 0 then by simp [h] else by simp [top_map h],
   sup := λ e₁ e₂,
   { to_fun := λ x, max (e₁ x) (e₂ x),
     eq_zero' := λ x h, e₁.eq_zero_iff.1 (ennreal.max_eq_zero_iff.1 h).1,
@@ -137,6 +139,7 @@ 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/analysis/specific_limits.lean

@@ -928,7 +928,7 @@ theorem exists_pos_sum_of_encodable {ε : ℝ≥0} (hε : ε ≠ 0) (ι) [encoda
   ∃ ε' : ι → ℝ≥0, (∀ i, 0 < ε' i) ∧ ∃c, has_sum ε' c ∧ c < ε :=
 let ⟨a, a0, aε⟩ := exists_between (pos_iff_ne_zero.2 hε) in
 let ⟨ε', hε', c, hc, hcε⟩ := pos_sum_of_encodable a0 ι in
-⟨ λi, ⟨ε' i, le_of_lt $ hε' i⟩, assume i, nnreal.coe_lt_coe.2 $ hε' i,
+⟨ λi, ⟨ε' i, le_of_lt $ hε' i⟩, assume i, nnreal.coe_lt_coe.1 $ hε' i,
   ⟨c, has_sum_le (assume i, le_of_lt $ hε' i) has_sum_zero hc ⟩, nnreal.has_sum_coe.1 hc,
    lt_of_le_of_lt (nnreal.coe_le_coe.1 hcε) aε ⟩
 

src/category_theory/sites/pretopology.lean

@@ -82,8 +82,7 @@ instance : order_top (pretopology C) :=
     has_isos := λ _ _ _ _, set.mem_univ _,
     pullbacks := λ _ _ _ _ _, set.mem_univ _,
     transitive := λ _ _ _ _ _, set.mem_univ _ },
-  le_top := λ K X S hS, set.mem_univ _,
-  ..pretopology.partial_order C }
+  le_top := λ K X S hS, set.mem_univ _ }
 
 instance : inhabited (pretopology C) := ⟨⊤⟩
 
@@ -202,8 +201,7 @@ instance : order_bot (pretopology C) :=
   begin
     rintro ⟨Y, f, hf, rfl⟩,
     exactI K.has_isos f,
-  end,
-  ..pretopology.partial_order C }
+  end }
 
 /-- The trivial pretopology induces the trivial grothendieck topology. -/
 lemma to_grothendieck_bot : to_grothendieck C ⊥ = ⊥ :=

src/category_theory/subobject/lattice.lean

@@ -201,8 +201,7 @@ instance order_top {X : C} : order_top (subobject X) :=
   begin
     refine quotient.ind' (λ f, _),
     exact ⟨mono_over.le_top f⟩,
-  end,
-  ..subobject.partial_order X}
+  end }
 
 instance {X : C} : inhabited (subobject X) := ⟨⊤⟩
 
@@ -266,8 +265,7 @@ instance order_bot {X : C} : order_bot (subobject X) :=
   begin
     refine quotient.ind' (λ f, _),
     exact ⟨mono_over.bot_le f⟩,
-  end,
-  ..subobject.partial_order X }
+  end }
 
 lemma bot_eq_initial_to {B : C} : (⊥ : subobject B) = subobject.mk (initial.to B) := rfl
 
@@ -342,7 +340,8 @@ instance {B : C} : semilattice_inf_top (subobject B) :=
   inf_le_left := inf_le_left,
   inf_le_right := inf_le_right,
   le_inf := le_inf,
-  ..subobject.order_top }
+  ..subobject.order_top,
+  ..subobject.partial_order B }
 
 lemma factors_left_of_inf_factors {A B : C} {X Y : subobject B} {f : A ⟶ B}
   (h : (X ⊓ Y).factors f) : X.factors f :=

src/combinatorics/colex.lean

@@ -351,8 +351,11 @@ def to_colex_rel_hom [linear_order α] :
 
 instance [linear_order α] : order_bot (finset.colex α) :=
 { bot := (∅ : finset α).to_colex,
-  bot_le := λ x, empty_to_colex_le,
-  ..(by apply_instance : partial_order (finset.colex α)) }
+  bot_le := λ x, empty_to_colex_le }
+
+instance [linear_order α] [fintype α] : order_top (finset.colex α) :=
+{ top := finset.univ.to_colex,
+  le_top := λ x, colex_le_of_subset (subset_univ _) }
 
 instance [linear_order α] : semilattice_inf_bot (finset.colex α) :=
 { ..finset.colex.order_bot,
@@ -363,8 +366,7 @@ instance [linear_order α] : semilattice_sup_bot (finset.colex α) :=
   ..(by apply_instance : semilattice_sup (finset.colex α)) }
 
 instance [linear_order α] [fintype α] : bounded_lattice (finset.colex α) :=
-{ top := finset.univ.to_colex,
-  le_top := λ x, colex_le_of_subset (subset_univ _),
+{ ..(by apply_instance : order_top (finset.colex α)),
   ..(by apply_instance : semilattice_sup (finset.colex α)),
   ..(by apply_instance : semilattice_inf_bot (finset.colex α)) }
 

src/control/lawful_fix.lean

@@ -51,7 +51,7 @@ variables (f : (Π a, part $ β a) →ₘ (Π a, part $ β a))
 
 lemma approx_mono' {i : ℕ} : fix.approx f i ≤ fix.approx f (succ i) :=
 begin
-  induction i, dsimp [approx], apply @bot_le _ _ (f ⊥),
+  induction i, dsimp [approx], apply @bot_le _ _ _ (f ⊥),
   intro, apply f.monotone, apply i_ih
 end
 

src/data/equiv/denumerable.lean

@@ -215,7 +215,7 @@ have wf : ∀ m : s, list.maximum t = m → ↑m < x,
   from λ m hmax, by simpa [hmt] using list.maximum_mem hmax,
 begin
   cases hmax : list.maximum t with m,
-  { exact ⟨0, le_antisymm (@bot_le s _ _)
+  { exact ⟨0, le_antisymm bot_le
       (le_of_not_gt (λ h, list.not_mem_nil (⊥ : s) $
         by rw [← list.maximum_eq_none.1 hmax, hmt]; exact h))⟩ },
   cases of_nat_surjective_aux m.2 with a ha,

src/data/finset/basic.lean

@@ -958,12 +958,15 @@ instance : lattice (finset α) :=
 @[simp] theorem sup_eq_union : ((⊔) : finset α → finset α → finset α) = (∪) := rfl
 @[simp] theorem inf_eq_inter : ((⊓) : finset α → finset α → finset α) = (∩) := rfl
 
+instance {α : Type u} : order_bot (finset α) :=
+{ bot := ∅, bot_le := empty_subset }
+
 instance : semilattice_inf_bot (finset α) :=
-{ bot := ∅, bot_le := empty_subset, ..finset.lattice }
+{ ..finset.order_bot, ..finset.lattice }
 
-@[simp] lemma bot_eq_empty : (⊥ : finset α) = ∅ := rfl
+@[simp] lemma bot_eq_empty {α : Type u} : (⊥ : finset α) = ∅ := rfl
 
-instance {α : Type*} [decidable_eq α] : semilattice_sup_bot (finset α) :=
+instance : semilattice_sup_bot (finset α) :=
 { ..finset.semilattice_inf_bot, ..finset.lattice }
 
 instance : distrib_lattice (finset α) :=

src/data/finset/locally_finite.lean

@@ -242,15 +242,15 @@ end
 end linear_order
 
 section order_top
-variables [order_top α] [locally_finite_order α]
+variables [preorder α] [order_top α] [locally_finite_order α]
 
 lemma _root_.bdd_below.finite {s : set α} (hs : bdd_below s) : s.finite :=
 hs.finite_of_bdd_above $ order_top.bdd_above s
 
 end order_top
 
 section order_bot
-variables [order_bot α] [locally_finite_order α]
+variables [preorder α] [order_bot α] [locally_finite_order α]
 
 lemma _root_.bdd_above.finite {s : set α} (hs : bdd_above s) : s.finite := hs.dual.finite