feat(order/hom/basic): add order_iso.with_{top,bot}_congr (#12264)

This adds:

* `with_bot.to_dual_top`
* `with_top.to_dual_bot`
* `order_iso.with_top_congr`
* `order_iso.with_bot_congr`

src/data/option/basic.lean

@@ -152,10 +152,14 @@ theorem map_none {α β} {f : α → β} : f <$> none = none := rfl
 
 theorem map_some {α β} {a : α} {f : α → β} : f <$> some a = some (f a) := rfl
 
+theorem map_coe {α β} {a : α} {f : α → β} : f <$> (a : option α) = ↑(f a) := rfl
+
 @[simp] theorem map_none' {f : α → β} : option.map f none = none := rfl
 
 @[simp] theorem map_some' {a : α} {f : α → β} : option.map f (some a) = some (f a) := rfl
 
+@[simp] theorem map_coe' {a : α} {f : α → β} : option.map f (a : option α) = ↑(f a) := rfl
+
 theorem map_eq_some {α β} {x : option α} {f : α → β} {b : β} :
   f <$> x = some b ↔ ∃ a, x = some a ∧ f a = b :=
 by cases x; simp

src/order/bounded_order.lean

@@ -490,6 +490,12 @@ option.rec h₁ h₂
 theorem coe_eq_coe {a b : α} : (a : with_bot α) = b ↔ a = b :=
 by rw [← option.some.inj_eq a b]; refl
 
+-- the `by exact` here forces the type of the equality to be `@eq (with_bot α)`
+@[simp] lemma map_bot (f : α → β) :
+  (by exact option.map f (⊥ : with_bot α)) = (⊥ : with_bot β) := rfl
+lemma map_coe (f : α → β) (a : α) :
+  (by exact option.map f (a : with_bot α)) = (f a : with_bot β) := rfl
+
 lemma ne_bot_iff_exists {x : with_bot α} : x ≠ ⊥ ↔ ∃ (a : α), ↑a = x :=
 option.ne_none_iff_exists
 
@@ -737,6 +743,12 @@ option.rec h₁ h₂
 theorem coe_eq_coe {a b : α} : (a : with_top α) = b ↔ a = b :=
 by rw [← option.some.inj_eq a b]; refl
 
+-- the `by exact` here forces the type of the equality to be `@eq (with_top α)`
+@[simp] lemma map_top (f : α → β) :
+  (by exact option.map f (⊤ : with_top α)) = (⊤ : with_top β) := rfl
+lemma map_coe (f : α → β) (a : α) :
+  (by exact option.map f (a : with_top α)) = (f a : with_top β) := rfl
+
 @[simp] theorem top_ne_coe {a : α} : ⊤ ≠ (a : with_top α) .
 @[simp] theorem coe_ne_top {a : α} : (a : with_top α) ≠ ⊤ .
 

src/order/hom/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
+import data.equiv.option
 import order.rel_iso
 import tactic.monotonicity.basic
 
@@ -711,6 +712,72 @@ lemma order_iso.map_sup [semilattice_sup α] [semilattice_sup β]
   f (x ⊔ y) = f x ⊔ f y :=
 f.dual.map_inf x y
 
+namespace with_bot
+
+/-- Taking the dual then adding `⊥` is the same as adding `⊤` then taking the dual. -/
+protected def to_dual_top [has_le α] : with_bot (order_dual α) ≃o order_dual (with_top α) :=
+order_iso.refl _
+
+@[simp] lemma to_dual_top_coe [has_le α] (a : α) :
+  with_bot.to_dual_top ↑(to_dual a) = to_dual (a : with_top α) := rfl
+@[simp] lemma to_dual_top_symm_coe [has_le α] (a : α) :
+  with_bot.to_dual_top.symm (to_dual (a : with_top α)) = ↑(to_dual a) := rfl
+
+end with_bot
+
+namespace with_top
+
+/-- Taking the dual then adding `⊤` is the same as adding `⊥` then taking the dual. -/
+protected def to_dual_bot [has_le α] : with_top (order_dual α) ≃o order_dual (with_bot α) :=
+order_iso.refl _
+
+@[simp] lemma to_dual_bot_coe [has_le α] (a : α) :
+  with_top.to_dual_bot ↑(to_dual a) = to_dual (a : with_bot α) := rfl
+@[simp] lemma to_dual_bot_symm_coe [has_le α] (a : α) :
+  with_top.to_dual_bot.symm (to_dual (a : with_bot α)) = ↑(to_dual a) := rfl
+
+end with_top
+
+namespace order_iso
+variables [partial_order α] [partial_order β] [partial_order γ]
+
+/-- A version of `equiv.option_congr` for `with_top`. -/
+@[simps apply]
+def with_top_congr (e : α ≃o β) : with_top α ≃o with_top β :=
+{ to_equiv := e.to_equiv.option_congr,
+  map_rel_iff' := λ x y,
+    by induction x using with_top.rec_top_coe; induction y using with_top.rec_top_coe; simp }
+
+@[simp] lemma with_top_congr_refl : (order_iso.refl α).with_top_congr = order_iso.refl _ :=
+rel_iso.to_equiv_injective equiv.option_congr_refl
+
+@[simp] lemma with_top_congr_symm (e : α ≃o β) : e.with_top_congr.symm = e.symm.with_top_congr :=
+rel_iso.to_equiv_injective e.to_equiv.option_congr_symm
+
+@[simp] lemma with_top_congr_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) :
+  e₁.with_top_congr.trans e₂.with_top_congr = (e₁.trans e₂).with_top_congr :=
+rel_iso.to_equiv_injective $ e₁.to_equiv.option_congr_trans e₂.to_equiv
+
+/-- A version of `equiv.option_congr` for `with_bot`. -/
+@[simps apply]
+def with_bot_congr (e : α ≃o β) :
+  with_bot α ≃o with_bot β :=
+{ to_equiv := e.to_equiv.option_congr,
+  map_rel_iff' := λ x y,
+    by induction x using with_bot.rec_bot_coe; induction y using with_bot.rec_bot_coe; simp }
+
+@[simp] lemma with_bot_congr_refl : (order_iso.refl α).with_bot_congr = order_iso.refl _ :=
+rel_iso.to_equiv_injective equiv.option_congr_refl
+
+@[simp] lemma with_bot_congr_symm (e : α ≃o β) : e.with_bot_congr.symm = e.symm.with_bot_congr :=
+rel_iso.to_equiv_injective e.to_equiv.option_congr_symm
+
+@[simp] lemma with_bot_congr_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) :
+  e₁.with_bot_congr.trans e₂.with_bot_congr = (e₁.trans e₂).with_bot_congr :=
+rel_iso.to_equiv_injective $ e₁.to_equiv.option_congr_trans e₂.to_equiv
+
+end order_iso
+
 section bounded_order
 
 variables [lattice α] [lattice β] [bounded_order α] [bounded_order β] (f : α ≃o β)