diff --git a/src/combinatorics/simple_graph/subgraph.lean b/src/combinatorics/simple_graph/subgraph.lean
index a84c33c6702b8..a095329f9c0f7 100644
--- a/src/combinatorics/simple_graph/subgraph.lean
+++ b/src/combinatorics/simple_graph/subgraph.lean
@@ -25,7 +25,7 @@ sub-relation of the adjacency relation of the simple graph.
 * `subgraph.is_spanning` for whether a subgraph is a spanning subgraph and
   `subgraph.is_induced` for whether a subgraph is an induced subgraph.
 
-* A `bounded_order (subgraph G)` instance, under the `subgraph` relation.
+* Instances for `lattice (subgraph G)` and `bounded_order (subgraph G)`.
 
 * `simple_graph.to_subgraph`: If a `simple_graph` is a subgraph of another, then you can turn it
   into a member of the larger graph's `simple_graph.subgraph` type.
diff --git a/src/data/fin/basic.lean b/src/data/fin/basic.lean
index 6e1f3096e9495..bcbae4537f13b 100644
--- a/src/data/fin/basic.lean
+++ b/src/data/fin/basic.lean
@@ -250,8 +250,9 @@ instance : bounded_order (fin (n + 1)) :=
 { top := last n,
   le_top := le_last,
   bot := 0,
-  bot_le := zero_le,
-  .. fin.linear_order, .. lattice_of_linear_order }
+  bot_le := zero_le }
+
+instance : lattice (fin (n + 1)) := lattice_of_linear_order
 
 lemma last_pos : (0 : fin (n + 2)) < last (n + 1) :=
 by simp [lt_iff_coe_lt_coe]
diff --git a/src/order/bounded_order.lean b/src/order/bounded_order.lean
index 0595ce62cfb55..7ee9080baa457 100644
--- a/src/order/bounded_order.lean
+++ b/src/order/bounded_order.lean
@@ -22,8 +22,6 @@ instances for `Prop` and `fun`.
 * `order_<top/bot> α`: Order with a top/bottom element.
 * `bounded_order α`: Order with a top and bottom element.
 * `with_<top/bot> α`: Equips `option α` with the order on `α` plus `none` as the top/bottom element.
-* `semilattice_<sup/inf>_<top/bot>`: Semilattice with a join/meet and a top/bottom element (all four
-  combinations). Typical examples include `ℕ`.
 * `is_compl x y`: In a bounded lattice, predicate for "`x` is a complement of `y`". Note that in a
   non distributive lattice, an element can have several complements.
 * `is_complemented α`: Typeclass stating that any element of a lattice has a complement.
@@ -255,11 +253,10 @@ inf_of_le_right bot_le
 
 end semilattice_inf_bot
 
-/-! ### Bounded lattice -/
+/-! ### Bounded order -/
 
 /-- A bounded order describes an order `(≤)` with a top and bottom element,
-  denoted `⊤` and `⊥` respectively. This allows for the interpretation
-  of all finite suprema and infima, taking `inf ∅ = ⊤` and `sup ∅ = ⊥`. -/
+  denoted `⊤` and `⊥` respectively. -/
 @[ancestor order_top order_bot]
 class bounded_order (α : Type u) [has_le α] extends order_top α, order_bot α.
 
@@ -276,17 +273,6 @@ begin
   { exact h'.symm }
 end
 
-lemma inf_eq_bot_iff_le_compl {α : Type u} [distrib_lattice α] [bounded_order α] {a b c : α}
-  (h₁ : b ⊔ c = ⊤) (h₂ : b ⊓ c = ⊥) : a ⊓ b = ⊥ ↔ a ≤ c :=
-⟨λ h,
-  calc a ≤ a ⊓ (b ⊔ c) : by simp [h₁]
-    ... = (a ⊓ b) ⊔ (a ⊓ c) : by simp [inf_sup_left]
-    ... ≤ c : by simp [h, inf_le_right],
-  λ h,
-  bot_unique $
-    calc a ⊓ b ≤ b ⊓ c : by { rw inf_comm, exact inf_le_inf_left _ h }
-      ... = ⊥ : h₂⟩
-
 /-- Propositions form a distributive lattice. -/
 instance Prop.distrib_lattice : distrib_lattice Prop :=
 { le           := λ a b, a → b,
@@ -1070,6 +1056,17 @@ end semilattice_inf_bot
 
 end disjoint
 
+lemma inf_eq_bot_iff_le_compl [distrib_lattice α] [bounded_order α] {a b c : α}
+  (h₁ : b ⊔ c = ⊤) (h₂ : b ⊓ c = ⊥) : a ⊓ b = ⊥ ↔ a ≤ c :=
+⟨λ h,
+  calc a ≤ a ⊓ (b ⊔ c) : by simp [h₁]
+    ... = (a ⊓ b) ⊔ (a ⊓ c) : by simp [inf_sup_left]
+    ... ≤ c : by simp [h, inf_le_right],
+  λ h,
+  bot_unique $
+    calc a ⊓ b ≤ b ⊓ c : by { rw inf_comm, exact inf_le_inf_left _ h }
+      ... = ⊥ : h₂⟩
+
 section is_compl
 
 /-- Two elements `x` and `y` are complements of each other if `x ⊔ y = ⊤` and `x ⊓ y = ⊥`. -/
diff --git a/src/order/filter/germ.lean b/src/order/filter/germ.lean
index 6d8496df2f31c..5fa7857b4b46e 100644
--- a/src/order/filter/germ.lean
+++ b/src/order/filter/germ.lean
@@ -43,7 +43,7 @@ For each of the following structures we prove that if `β` has this structure, t
 * one-operation algebraic structures up to `comm_group`;
 * `mul_zero_class`, `distrib`, `semiring`, `comm_semiring`, `ring`, `comm_ring`;
 * `mul_action`, `distrib_mul_action`, `module`;
-* `preorder`, `partial_order`, and `lattice` structures up to `bounded_order`;
+* `preorder`, `partial_order`, and `lattice` structures, as well as `bounded_order`;
 * `ordered_cancel_comm_monoid` and `ordered_cancel_add_comm_monoid`.
 
 ## Tags