feat(data/real/nnreal): define nnreal.gi : galois_insertion of_real coe (#1699)

Author: urkud

src/data/real/nnreal.lean

@@ -34,6 +34,9 @@ protected def of_real (r : ℝ) : ℝ≥0 := ⟨max r 0, le_max_right _ _⟩
 lemma coe_of_real (r : ℝ) (hr : 0 ≤ r) : (nnreal.of_real r : ℝ) = r :=
 max_eq_left hr
 
+lemma le_coe_of_real (r : ℝ) : r ≤ nnreal.of_real r :=
+le_max_left r 0
+
 lemma coe_nonneg (r : nnreal) : (0 : ℝ) ≤ r := r.2
 
 instance : has_zero ℝ≥0  := ⟨⟨0, le_refl 0⟩⟩
@@ -93,6 +96,19 @@ decidable_linear_order.lift (coe : ℝ≥0 → ℝ) subtype.val_injective (by ap
 @[elim_cast] protected lemma coe_lt {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) < r₂ ↔ r₁ < r₂ := iff.rfl
 @[elim_cast] protected lemma coe_pos {r : ℝ≥0} : (0 : ℝ) < r ↔ 0 < r := iff.rfl
 
+protected lemma coe_mono : monotone (coe : ℝ≥0 → ℝ) := λ _ _, nnreal.coe_le.2
+
+protected lemma of_real_mono : monotone nnreal.of_real :=
+λ x y h, max_le_max h (le_refl 0)
+
+@[simp] lemma of_real_coe {r : ℝ≥0} : nnreal.of_real r = r :=
+nnreal.eq $ max_eq_left r.2
+
+/-- `nnreal.of_real` and `coe : ℝ≥0 → ℝ` form a Galois insertion. -/
+protected def gi : galois_insertion nnreal.of_real coe :=
+galois_insertion.monotone_intro nnreal.coe_mono nnreal.of_real_mono
+  le_coe_of_real (λ _, of_real_coe)
+
 instance : order_bot ℝ≥0 :=
 { bot := ⊥, bot_le := assume ⟨a, h⟩, h, .. nnreal.decidable_linear_order }
 
@@ -246,9 +262,6 @@ by simpa [-of_real_pos] using (not_iff_not.2 (@of_real_pos r))
 lemma of_real_of_nonpos {r : ℝ} : r ≤ 0 → nnreal.of_real r = 0 :=
 of_real_eq_zero.2
 
-@[simp] lemma of_real_coe {r : nnreal} : nnreal.of_real r = r :=
-nnreal.eq $ by simp [nnreal.of_real]
-
 @[simp] lemma of_real_le_of_real_iff {r p : ℝ} (hp : 0 ≤ p) :
   nnreal.of_real r ≤ nnreal.of_real p ↔ r ≤ p :=
 by simp [nnreal.coe_le.symm, nnreal.of_real, hp]
@@ -270,19 +283,13 @@ lemma of_real_add_of_real {r p : ℝ} (hr : 0 ≤ r) (hp : 0 ≤ p) :
 (of_real_add hr hp).symm
 
 lemma of_real_le_of_real {r p : ℝ} (h : r ≤ p) : nnreal.of_real r ≤ nnreal.of_real p :=
-nnreal.coe_le.2 $ max_le_max h $ le_refl _
+nnreal.of_real_mono h
 
 lemma of_real_add_le {r p : ℝ} : nnreal.of_real (r + p) ≤ nnreal.of_real r + nnreal.of_real p :=
 nnreal.coe_le.1 $ max_le (add_le_add (le_max_left _ _) (le_max_left _ _)) nnreal.zero_le_coe
 
 lemma of_real_le_iff_le_coe {r : ℝ} {p : nnreal} : nnreal.of_real r ≤ p ↔ r ≤ ↑p :=
-begin
-  cases le_total 0 r,
-  { rw [← nnreal.coe_le, nnreal.coe_of_real r h] },
-  { rw [of_real_eq_zero.2 h], split,
-    intro, exact le_trans h (coe_nonneg _),
-    intro, exact zero_le _ }
-end
+nnreal.gi.gc r p
 
 lemma le_of_real_iff_coe_le {r : nnreal} {p : ℝ} (hp : p ≥ 0) : r ≤ nnreal.of_real p ↔ ↑r ≤ p :=
 by rw [← nnreal.coe_le, nnreal.coe_of_real p hp]

src/order/galois_connection.lean

@@ -192,6 +192,15 @@ structure galois_insertion {α β : Type*} [preorder α] [preorder β] (l : α 
 (le_l_u : ∀x, x ≤ l (u x))
 (choice_eq : ∀a h, choice a h = l a)
 
+/-- A constructor for a Galois insertion with the trivial `choice` function. -/
+def galois_insertion.monotone_intro {α β : Type*} [preorder α] [preorder β] {l : α → β} {u : β → α}
+  (hu : monotone u) (hl : monotone l) (hul : ∀ a, a ≤ u (l a)) (hlu : ∀ b, l (u b) = b) :
+  galois_insertion l u :=
+{ choice := λ x _, l x,
+  gc := galois_connection.monotone_intro hu hl hul (λ b, le_of_eq (hlu b)),
+  le_l_u := λ b, le_of_eq $ (hlu b).symm,
+  choice_eq := λ _ _, rfl }
+
 /-- Makes a Galois insertion from an order-preserving bijection. -/
 protected def order_iso.to_galois_insertion [preorder α] [preorder β] (oi : @order_iso α β (≤) (≤)) : 
 @galois_insertion α β _ _ (oi) (oi.symm) :=