feat(data/real/enat_ennreal): define coercion from enat to ennreal (

#17207)

src/algebra/order/ring.lean

@@ -550,7 +550,11 @@ lemma one_lt_two : (1 : α) < 2 := lt_add_one _
 lemma lt_two_mul_self (ha : 0 < a) : a < 2 * a := lt_mul_of_one_lt_left ha one_lt_two
 
 lemma nat.strict_mono_cast : strict_mono (coe : ℕ → α) :=
-strict_mono_nat_of_lt_succ $ λ n, by rw [nat.cast_succ]; apply lt_add_one
+strict_mono_nat_of_lt_succ $ λ n, by { rw [nat.cast_succ], apply lt_add_one }
+
+/-- `coe : ℕ → α` as an `order_embedding` -/
+@[simps { fully_applied := ff }] def nat.cast_order_embedding : ℕ ↪o α :=
+order_embedding.of_strict_mono coe nat.strict_mono_cast
 
 @[priority 100] -- see Note [lower instance priority]
 instance strict_ordered_semiring.to_no_max_order : no_max_order α :=

src/algebra/order/sub/with_top.lean

@@ -10,7 +10,7 @@ import algebra.order.monoid.with_top
 # Lemma about subtraction in ordered monoids with a top element adjoined.
 -/
 
-variables {α : Type*}
+variables {α β : Type*}
 
 namespace with_top
 
@@ -30,6 +30,13 @@ instance : has_sub (with_top α) :=
 @[simp] lemma top_sub_coe {a : α} : (⊤ : with_top α) - a = ⊤ := rfl
 @[simp] lemma sub_top {a : with_top α} : a - ⊤ = 0 := by { cases a; refl }
 
+lemma map_sub [has_sub β] [has_zero β] {f : α → β} (h : ∀ x y, f (x - y) = f x - f y)
+  (h₀ : f 0 = 0) :
+  ∀ x y : with_top α, (x - y).map f = x.map f - y.map f
+| _ ⊤ := by simp only [h₀, sub_top, with_top.map_zero, coe_zero, map_top]
+| ⊤ (x : α) := rfl
+| (x : α) (y : α) := by simp only [← coe_sub, map_coe, h]
+
 end
 
 variables [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α]

src/data/nat/cast.lean

@@ -72,6 +72,19 @@ zero_lt_one.trans_le $ le_add_of_nonneg_left n.cast_nonneg
 
 end ordered_semiring
 
+/-- A version of `nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work
+for `ℕ∞` and `ℝ≥0∞`, so we use type-specific lemmas for these types. -/
+@[simp, norm_cast] lemma cast_tsub [canonically_ordered_comm_semiring α] [has_sub α]
+  [has_ordered_sub α] [contravariant_class α α (+) (≤)] (m n : ℕ) :
+  ↑(m - n) = (m - n : α) :=
+begin
+  cases le_total m n with h h,
+  { rw [tsub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le],
+    exact mono_cast h },
+  { rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩,
+    rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right] }
+end
+
 section strict_ordered_semiring
 variables [strict_ordered_semiring α] [nontrivial α]
 

src/data/real/enat_ennreal.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import data.real.ennreal
+import data.enat.basic
+
+/-!
+# Coercion from `ℕ∞` to `ℝ≥0∞`
+
+In this file we define a coercion from `ℕ∞` to `ℝ≥0∞` and prove some basic lemmas about this map.
+-/
+
+open_locale classical nnreal ennreal
+noncomputable theory
+
+namespace enat
+
+variables {m n : ℕ∞}
+
+instance has_coe_ennreal : has_coe_t ℕ∞ ℝ≥0∞ := ⟨with_top.map coe⟩
+
+@[simp] lemma map_coe_nnreal : with_top.map (coe : ℕ → ℝ≥0) = (coe : ℕ∞ → ℝ≥0∞) := rfl
+
+/-- Coercion `ℕ∞ → ℝ≥0∞` as an `order_embedding`. -/
+@[simps { fully_applied := ff }] def to_ennreal_order_embedding : ℕ∞ ↪o ℝ≥0∞ :=
+nat.cast_order_embedding.with_top_map
+
+/-- Coercion `ℕ∞ → ℝ≥0∞` as a ring homomorphism. -/
+@[simps { fully_applied := ff }] def to_ennreal_ring_hom : ℕ∞ →+* ℝ≥0∞ :=
+(nat.cast_ring_hom ℝ≥0).with_top_map nat.cast_injective
+
+@[simp, norm_cast] lemma coe_ennreal_top : ((⊤ : ℕ∞) : ℝ≥0∞) = ⊤ := rfl
+@[simp, norm_cast] lemma coe_ennreal_coe (n : ℕ) : ((n : ℕ∞) : ℝ≥0∞) = n := rfl
+
+@[simp, norm_cast] lemma coe_ennreal_le : (m : ℝ≥0∞) ≤ n ↔ m ≤ n :=
+to_ennreal_order_embedding.le_iff_le
+
+@[simp, norm_cast] lemma coe_ennreal_lt : (m : ℝ≥0∞) < n ↔ m < n :=
+to_ennreal_order_embedding.lt_iff_lt
+
+@[mono] lemma coe_ennreal_mono : monotone (coe : ℕ∞ → ℝ≥0∞) := to_ennreal_order_embedding.monotone
+
+@[mono] lemma coe_ennreal_strict_mono : strict_mono (coe : ℕ∞ → ℝ≥0∞) :=
+to_ennreal_order_embedding.strict_mono
+
+@[simp, norm_cast] lemma coe_ennreal_zero : ((0 : ℕ∞) : ℝ≥0∞) = 0 := map_zero to_ennreal_ring_hom
+
+@[simp] lemma coe_ennreal_add (m n : ℕ∞) : ↑(m + n) = (m + n : ℝ≥0∞) :=
+map_add to_ennreal_ring_hom m n
+
+@[simp] lemma coe_ennreal_one : ((1 : ℕ∞) : ℝ≥0∞) = 1 := map_one to_ennreal_ring_hom
+
+@[simp] lemma coe_ennreal_bit0 (n : ℕ∞) : ↑(bit0 n) = bit0 (n : ℝ≥0∞) := coe_ennreal_add n n
+
+@[simp] lemma coe_ennreal_bit1 (n : ℕ∞) : ↑(bit1 n) = bit1 (n : ℝ≥0∞) :=
+map_bit1 to_ennreal_ring_hom n
+
+@[simp] lemma coe_ennreal_mul (m n : ℕ∞) : ↑(m * n) = (m * n : ℝ≥0∞) :=
+map_mul to_ennreal_ring_hom m n
+
+@[simp] lemma coe_ennreal_min (m n : ℕ∞) : ↑(min m n) = (min m n : ℝ≥0∞) := coe_ennreal_mono.map_min
+@[simp] lemma coe_ennreal_max (m n : ℕ∞) : ↑(max m n) = (max m n : ℝ≥0∞) := coe_ennreal_mono.map_max
+
+@[simp] lemma coe_ennreal_sub (m n : ℕ∞) : ↑(m - n) = (m - n : ℝ≥0∞) :=
+with_top.map_sub nat.cast_tsub nat.cast_zero m n
+
+end enat

src/data/real/ennreal.lean

@@ -805,6 +805,9 @@ by { cases a; cases b; simp [← with_top.coe_sub] }
 lemma sub_ne_top (ha : a ≠ ∞) : a - b ≠ ∞ :=
 mt sub_eq_top_iff.mp $ mt and.left ha
 
+@[simp, norm_cast] lemma nat_cast_sub (m n : ℕ) : ↑(m - n) = (m - n : ℝ≥0∞) :=
+by rw [← coe_nat, nat.cast_tsub, coe_sub, coe_nat, coe_nat]
+
 protected lemma sub_eq_of_eq_add (hb : b ≠ ∞) : a = c + b → a - b = c :=
 (cancel_of_ne hb).tsub_eq_of_eq_add