diff --git a/src/algebra/pointwise.lean b/src/algebra/pointwise.lean
index 1c691d5185ca4..079194f766b2a 100644
--- a/src/algebra/pointwise.lean
+++ b/src/algebra/pointwise.lean
@@ -812,7 +812,7 @@ section monoid
 
 /-- An alias for `set α`, which has a semiring structure given by `∪` as "addition" and pointwise
   multiplication `*` as "multiplication". -/
-@[derive inhabited] def set_semiring (α : Type*) : Type* := set α
+@[derive [inhabited, partial_order, order_bot]] def set_semiring (α : Type*) : Type* := set α
 
 /-- The identitiy function `set α → set_semiring α`. -/
 protected def up (s : set α) : set_semiring α := s
@@ -821,6 +821,14 @@ protected def set_semiring.down (s : set_semiring α) : set α := s
 @[simp] protected lemma down_up {s : set α} : s.up.down = s := rfl
 @[simp] protected lemma up_down {s : set_semiring α} : s.down.up = s := rfl
 
+/- This lemma is not tagged `simp`, since otherwise the linter complains. -/
+lemma up_le_up {s t : set α} : s.up ≤ t.up ↔ s ⊆ t := iff.rfl
+/- This lemma is not tagged `simp`, since otherwise the linter complains. -/
+lemma up_lt_up {s t : set α} : s.up < t.up ↔ s ⊂ t := iff.rfl
+
+@[simp] lemma down_subset_down {s t : set_semiring α} : s.down ⊆ t.down ↔ s ≤ t := iff.rfl
+@[simp] lemma down_ssubset_down {s t : set_semiring α} : s.down ⊂ t.down ↔ s < t := iff.rfl
+
 instance set_semiring.add_comm_monoid : add_comm_monoid (set_semiring α) :=
 { add := λ s t, (s ∪ t : set α),
   zero := (∅ : set α),