chore(order/galois_connection): define with_bot.gi_get_or_else_bot (#…

…4781)

This Galois insertion can be used to golf proofs about
`polynomial.degree` vs `polynomial.nat_degree`.

src/data/option/basic.lean

@@ -28,6 +28,8 @@ theorem get_of_mem {a : α} : ∀ {o : option α} (h : is_some o), a ∈ o → o
 
 @[simp] lemma get_or_else_some (x y : α) : option.get_or_else (some x) y = x := rfl
 
+@[simp] lemma get_or_else_coe (x y : α) : option.get_or_else ↑x y = x := rfl
+
 lemma get_or_else_of_ne_none {x : option α} (hx : x ≠ none) (y : α) : some (x.get_or_else y) = x :=
 by cases x; [contradiction, rw get_or_else_some]
 

src/order/bounded_lattice.lean

@@ -488,6 +488,12 @@ lemma le_coe_get_or_else [preorder α] : ∀ (a : with_bot α) (b : α), a ≤ a
 | (some a) b := le_refl a
 | none     b := λ _ h, option.no_confusion h
 
+@[simp] lemma get_or_else_bot (a : α) : option.get_or_else (⊥ : with_bot α) a = a := rfl
+
+lemma get_or_else_bot_le_iff [order_bot α] {a : with_bot α} {b : α} :
+  a.get_or_else ⊥ ≤ b ↔ a ≤ b :=
+by cases a; simp [none_eq_bot, some_eq_coe]
+
 instance linear_order [linear_order α] : linear_order (with_bot α) :=
 { le_total := λ o₁ o₂, begin
     cases o₁ with a, {exact or.inl bot_le},

src/order/galois_connection.lean

@@ -547,3 +547,12 @@ def lift_complete_lattice [complete_lattice β] (gi : galois_coinsertion l u) :
 end lift
 
 end galois_coinsertion
+
+/-- If `α` is a partial order with bottom element (e.g., `ℕ`, `ℝ≥0`), then
+`λ o : with_bot α, o.get_or_else ⊥` and coercion form a Galois insertion. -/
+def with_bot.gi_get_or_else_bot [order_bot α] :
+  galois_insertion (λ o : with_bot α, o.get_or_else ⊥) coe :=
+{ gc := λ a b, with_bot.get_or_else_bot_le_iff,
+  le_l_u := λ a, le_rfl,
+  choice := λ o ho, _,
+  choice_eq := λ _ _, rfl }