refactor(data/real/ennreal): redefine ennreal.to_nnreal in terms of…

… `with_top.untop'` (#15247)

* redefine `ennreal.to_nnreal` as `with_top.untop' 0`;
* use lambda function instead of `id` for identity coercions of `nat` and `int`;
* move `with_top.add_monoid_with_one` and `with_bot.add_monoid_with_one` to `algebra.order.monoid`, add commutative version;
* generalize `ennreal.to_nnreal_mul` to `with_top`.

src/algebra/order/monoid.lean

@@ -1045,6 +1045,15 @@ instance [add_monoid α] : add_monoid (with_top α) :=
 instance [add_comm_monoid α] : add_comm_monoid (with_top α) :=
 { ..with_top.add_monoid, ..with_top.add_comm_semigroup }
 
+instance [add_monoid_with_one α] : add_monoid_with_one (with_top α) :=
+{ nat_cast := λ n, ↑(n : α),
+  nat_cast_zero := by rw [nat.cast_zero, with_top.coe_zero],
+  nat_cast_succ := λ n, by rw [nat.cast_add_one, with_top.coe_add, with_top.coe_one],
+  .. with_top.has_one, .. with_top.add_monoid }
+
+instance [add_comm_monoid_with_one α] : add_comm_monoid_with_one (with_top α) :=
+{ .. with_top.add_monoid_with_one, .. with_top.add_comm_monoid }
+
 instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (with_top α) :=
 { add_le_add_left :=
     begin
@@ -1137,6 +1146,10 @@ instance [add_comm_semigroup α] : add_comm_semigroup (with_bot α) := with_top.
 instance [add_zero_class α] : add_zero_class (with_bot α) := with_top.add_zero_class
 instance [add_monoid α] : add_monoid (with_bot α) := with_top.add_monoid
 instance [add_comm_monoid α] : add_comm_monoid (with_bot α) := with_top.add_comm_monoid
+instance [add_monoid_with_one α] : add_monoid_with_one (with_bot α) := with_top.add_monoid_with_one
+
+instance [add_comm_monoid_with_one α] : add_comm_monoid_with_one (with_bot α) :=
+with_top.add_comm_monoid_with_one
 
 instance [has_zero α] [has_one α] [has_le α] [zero_le_one_class α] :
   zero_le_one_class (with_bot α) :=

src/algebra/order/ring.lean

@@ -1567,16 +1567,7 @@ The main results of this section are `with_top.canonically_ordered_comm_semiring
 
 namespace with_top
 
-instance [nonempty α] : nontrivial (with_top α) :=
-option.nontrivial
-
-instance [add_monoid_with_one α] : add_monoid_with_one (with_top α) :=
-{ nat_cast := λ n, ((n : α) : with_top α),
-  nat_cast_zero := show (((0 : ℕ) : α) : with_top α) = 0, by simp,
-  nat_cast_succ :=
-    show ∀ n, (((n + 1 : ℕ) : α) : with_top α) = (((n : ℕ) : α) : with_top α) + 1,
-    by simp [with_top.coe_add],
-  .. with_top.add_monoid, .. with_top.has_one }
+instance [nonempty α] : nontrivial (with_top α) := option.nontrivial
 
 variable [decidable_eq α]
 
@@ -1586,7 +1577,7 @@ variables [has_zero α] [has_mul α]
 
 instance : mul_zero_class (with_top α) :=
 { zero := 0,
-  mul := λm n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
+  mul := λ m n, if m = 0 ∨ n = 0 then 0 else m.bind (λa, n.bind $ λb, ↑(a * b)),
   zero_mul := assume a, if_pos $ or.inl rfl,
   mul_zero := assume a, if_pos $ or.inr rfl }
 
@@ -1636,6 +1627,15 @@ begin
   simp only [← coe_mul, coe_lt_top]
 end
 
+@[simp] lemma untop'_zero_mul (a b : with_top α) : (a * b).untop' 0 = a.untop' 0 * b.untop' 0 :=
+begin
+  by_cases ha : a = 0, { rw [ha, zero_mul, ← coe_zero, untop'_coe, zero_mul] },
+  by_cases hb : b = 0, { rw [hb, mul_zero, ← coe_zero, untop'_coe, mul_zero] },
+  induction a using with_top.rec_top_coe, { rw [top_mul hb, untop'_top, zero_mul] },
+  induction b using with_top.rec_top_coe, { rw [mul_top ha, untop'_top, mul_zero] },
+  rw [← coe_mul, untop'_coe, untop'_coe, untop'_coe]
+end
+
 end mul_zero_class
 
 /-- `nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `= 0 * ⊤ = 0`. -/
@@ -1726,8 +1726,8 @@ that derives from both `non_assoc_non_unital_semiring` and `canonically_ordered_
 of which are required for distributivity. -/
 instance [nontrivial α] : comm_semiring (with_top α) :=
 { right_distrib   := distrib',
-  left_distrib    := assume a b c, by rw [mul_comm, distrib', mul_comm b, mul_comm c]; refl,
-  .. with_top.add_monoid_with_one, .. with_top.add_comm_monoid, .. with_top.comm_monoid_with_zero }
+  left_distrib    := λ a b c, by { rw [mul_comm, distrib', mul_comm b, mul_comm c], refl },
+  .. with_top.add_comm_monoid_with_one, .. with_top.comm_monoid_with_zero }
 
 instance [nontrivial α] : canonically_ordered_comm_semiring (with_top α) :=
 { .. with_top.comm_semiring,
@@ -1747,16 +1747,7 @@ end with_top
 
 namespace with_bot
 
-instance [nonempty α] : nontrivial (with_bot α) :=
-option.nontrivial
-
-instance [add_monoid_with_one α] : add_monoid_with_one (with_bot α) :=
-{ nat_cast := λ n, ((n : α) : with_bot α),
-  nat_cast_zero := show (((0 : ℕ) : α) : with_bot α) = 0, by simp,
-  nat_cast_succ :=
-    show ∀ n, (((n + 1 : ℕ) : α) : with_bot α) = (((n : ℕ) : α) : with_bot α) + 1,
-    by simp [with_bot.coe_add],
-  .. with_bot.add_monoid, .. with_bot.has_one }
+instance [nonempty α] : nontrivial (with_bot α) := option.nontrivial
 
 variable [decidable_eq α]
 

src/data/int/basic.lean

@@ -56,7 +56,7 @@ instance : comm_ring int :=
   nat_cast       := int.of_nat,
   nat_cast_zero  := rfl,
   nat_cast_succ  := λ n, rfl,
-  int_cast       := id,
+  int_cast       := λ n, n,
   int_cast_of_nat := λ n, rfl,
   int_cast_neg_succ_of_nat := λ n, rfl,
   zsmul          := (*),

src/data/nat/basic.lean

@@ -44,7 +44,7 @@ instance : comm_semiring ℕ :=
   zero_mul       := nat.zero_mul,
   mul_zero       := nat.mul_zero,
   mul_comm       := nat.mul_comm,
-  nat_cast       := id,
+  nat_cast       := λ n, n,
   nat_cast_zero  := rfl,
   nat_cast_succ  := λ n, rfl,
   nsmul          := λ m n, m * n,

src/data/real/ennreal.lean

@@ -107,9 +107,7 @@ instance : can_lift ℝ≥0∞ ℝ≥0 :=
 @[simp] lemma some_eq_coe (a : ℝ≥0) : (some a : ℝ≥0∞) = (↑a : ℝ≥0∞) := rfl
 
 /-- `to_nnreal x` returns `x` if it is real, otherwise 0. -/
-protected def to_nnreal : ℝ≥0∞ → ℝ≥0
-| (some r) := r
-| none := 0
+protected def to_nnreal : ℝ≥0∞ → ℝ≥0 := with_top.untop' 0
 
 /-- `to_real x` returns `x` if it is real, `0` otherwise. -/
 protected def to_real (a : ℝ≥0∞) : real := coe (a.to_nnreal)
@@ -1653,24 +1651,11 @@ lemma of_real_div_of_pos {x y : ℝ} (hy : 0 < y) :
   ennreal.of_real (x / y) = ennreal.of_real x / ennreal.of_real y :=
 by rw [div_eq_mul_inv, div_eq_mul_inv, of_real_mul' (inv_nonneg.2 hy.le), of_real_inv_of_pos hy]
 
-lemma to_nnreal_mul_top (a : ℝ≥0∞) : ennreal.to_nnreal (a * ∞) = 0 :=
-begin
-  by_cases h : a = 0,
-  { rw [h, zero_mul, zero_to_nnreal] },
-  { rw [mul_top, if_neg h, top_to_nnreal] }
-end
-
-lemma to_nnreal_top_mul (a : ℝ≥0∞) : ennreal.to_nnreal (∞ * a) = 0 :=
-by rw [mul_comm, to_nnreal_mul_top]
-
 @[simp] lemma to_nnreal_mul {a b : ℝ≥0∞} : (a * b).to_nnreal = a.to_nnreal * b.to_nnreal :=
-begin
-  induction a using with_top.rec_top_coe,
-  { rw [to_nnreal_top_mul, top_to_nnreal, zero_mul] },
-  induction b using with_top.rec_top_coe,
-  { rw [to_nnreal_mul_top, top_to_nnreal, mul_zero] },
-  simp only [to_nnreal_coe, ← coe_mul]
-end
+with_top.untop'_zero_mul a b
+
+lemma to_nnreal_mul_top (a : ℝ≥0∞) : ennreal.to_nnreal (a * ∞) = 0 := by simp
+lemma to_nnreal_top_mul (a : ℝ≥0∞) : ennreal.to_nnreal (∞ * a) = 0 := by simp
 
 @[simp] lemma smul_to_nnreal (a : ℝ≥0) (b : ℝ≥0∞) :
   (a • b).to_nnreal = a * b.to_nnreal :=