feat(order/bounded_order): two lemmas about the interaction between m…

…onotonicity and map with_bot/top (#15341)

Pulled out of #15294, that I ~plan to~ closed.

src/order/bounded_order.lean

@@ -668,6 +668,12 @@ instance [partial_order α] : partial_order (with_bot α) :=
   end,
   .. with_bot.preorder }
 
+lemma map_le_iff [preorder α] [preorder β] (f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
+  ∀ (a b : with_bot α), a.map f ≤ b.map f ↔ a ≤ b
+| ⊥       _       := by simp only [map_bot, bot_le]
+| (a : α) ⊥       := by simp only [map_coe, map_bot, coe_ne_bot, not_coe_le_bot _]
+| (a : α) (b : α) := by simpa using mono_iff
+
 lemma le_coe_get_or_else [preorder α] : ∀ (a : with_bot α) (b : α), a ≤ a.get_or_else b
 | (some a) b := le_refl a
 | none     b := λ _ h, option.no_confusion h
@@ -970,6 +976,11 @@ instance [partial_order α] : partial_order (with_top α) :=
   end,
   .. with_top.preorder }
 
+lemma map_le_iff [preorder α] [preorder β] (f : α → β)
+  (a b : with_top α) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
+  a.map f ≤ b.map f ↔ a ≤ b :=
+@with_bot.map_le_iff αᵒᵈ βᵒᵈ _ _ f (λ a b, mono_iff) b a
+
 instance [semilattice_inf α] : semilattice_inf (with_top α) :=
 { inf          := option.lift_or_get (⊓),
   inf_le_left  := λ o₁ o₂ a ha,

src/order/hom/basic.lean

@@ -427,8 +427,7 @@ protected def dual : αᵒᵈ ↪o βᵒᵈ :=
 @[simps { fully_applied := ff }]
 protected def with_bot_map (f : α ↪o β) : with_bot α ↪o with_bot β :=
 { to_fun := with_bot.map f,
-  map_rel_iff' := λ a b, by cases a; cases b; simp [with_bot.none_eq_bot, with_bot.some_eq_coe,
-    with_bot.not_coe_le_bot],
+  map_rel_iff' := with_bot.map_le_iff f (λ a b, f.map_rel_iff),
   .. f.to_embedding.option_map }
 
 /-- A version of `with_top.map` for order embeddings. -/