chore(data/real/nnreal): Golf (#16307)

Generalize various lemmas to `linear_ordered_semifield` or weaker so that they apply to `nnreal`. Golf the `nnreal` API using them.

src/algebra/big_operators/ring.lean

@@ -70,7 +70,7 @@ by simp
 
 end semiring
 
-lemma sum_div [division_ring β] {s : finset α} {f : α → β} {b : β} :
+lemma sum_div [division_semiring β] {s : finset α} {f : α → β} {b : β} :
   (∑ x in s, f x) / b = ∑ x in s, f x / b :=
 by simp only [div_eq_mul_inv, sum_mul]
 

src/algebra/order/field.lean

@@ -451,6 +451,8 @@ end
 
 lemma one_half_lt_one : (1 / 2 : α) < 1 := half_lt_self zero_lt_one
 
+lemma two_inv_lt_one : (2⁻¹ : α) < 1 := (one_div _).symm.trans_lt one_half_lt_one
+
 lemma left_lt_add_div_two : a < (a + b) / 2 ↔ a < b := by simp [lt_div_iff, mul_two]
 
 lemma add_div_two_lt_right : (a + b) / 2 < b ↔ a < b := by simp [div_lt_iff, mul_two]

src/algebra/order/field_defs.lean

@@ -56,3 +56,8 @@ instance canonically_linear_ordered_semifield.to_linear_ordered_comm_group_with_
   [canonically_linear_ordered_semifield α] : linear_ordered_comm_group_with_zero α :=
 { mul_le_mul_left := λ a b h c, mul_le_mul_of_nonneg_left h $ zero_le _,
   ..‹canonically_linear_ordered_semifield α› }
+
+@[priority 100] -- See note [lower instance priority]
+instance canonically_linear_ordered_semifield.to_canonically_linear_ordered_add_monoid
+  [canonically_linear_ordered_semifield α] : canonically_linear_ordered_add_monoid α :=
+{ ..‹canonically_linear_ordered_semifield α› }

src/algebra/order/group.lean

@@ -58,11 +58,9 @@ instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u)
   le_of_mul_le_mul_left := λ a b c, (mul_le_mul_iff_left a).mp,
   ..s }
 
-@[priority 100, to_additive]
-instance ordered_comm_group.has_exists_mul_of_le (α : Type u)
-  [ordered_comm_group α] :
-  has_exists_mul_of_le α :=
-⟨λ a b hab, ⟨b * a⁻¹, (mul_inv_cancel_comm_assoc a b).symm⟩⟩
+@[priority 100, to_additive] -- See note [lower instance priority]
+instance group.has_exists_mul_of_le (α : Type u) [group α] [has_le α] : has_exists_mul_of_le α :=
+⟨λ a b hab, ⟨a⁻¹ * b, (mul_inv_cancel_left _ _).symm⟩⟩
 
 
 @[to_additive] instance [ordered_comm_group α] : ordered_comm_group αᵒᵈ :=
@@ -818,15 +816,9 @@ end variable_names
 section densely_ordered
 variables [densely_ordered α] {a b c : α}
 
-@[to_additive]
-lemma le_of_forall_one_lt_le_mul (h : ∀ ε : α, 1 < ε → a ≤ b * ε) : a ≤ b :=
-le_of_forall_le_of_dense $ λ c hc,
-calc a ≤ b * (b⁻¹ * c) : h _ (lt_inv_mul_iff_lt.mpr hc)
-   ... = c             : mul_inv_cancel_left b c
-
 @[to_additive]
 lemma le_of_forall_lt_one_mul_le (h : ∀ ε < 1, a * ε ≤ b) : a ≤ b :=
-@le_of_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _ h
+@le_of_forall_one_lt_le_mul αᵒᵈ _ _ _ _ _ _ _ _ h
 
 @[to_additive]
 lemma le_of_forall_one_lt_div_le (h : ∀ ε : α, 1 < ε → a / ε ≤ b) : a ≤ b :=

src/algebra/order/monoid.lean

@@ -95,6 +95,25 @@ export has_exists_mul_of_le (exists_mul_of_le)
 
 export has_exists_add_of_le (exists_add_of_le)
 
+section has_exists_mul_of_le
+variables [linear_order α] [densely_ordered α] [monoid α] [has_exists_mul_of_le α]
+  [covariant_class α α (*) (<)] [contravariant_class α α (*) (<)] {a b : α}
+
+@[to_additive]
+lemma le_of_forall_one_lt_le_mul (h : ∀ ε : α, 1 < ε → a ≤ b * ε) : a ≤ b :=
+le_of_forall_le_of_dense $ λ x hxb, by { obtain ⟨ε, rfl⟩ := exists_mul_of_le hxb.le,
+  exact h _ ((lt_mul_iff_one_lt_right' b).1 hxb) }
+
+@[to_additive]
+lemma le_of_forall_one_lt_lt_mul' (h : ∀ ε : α, 1 < ε → a < b * ε) : a ≤ b :=
+le_of_forall_one_lt_le_mul $ λ ε hε, (h _ hε).le
+
+@[to_additive]
+lemma le_iff_forall_one_lt_lt_mul' : a ≤ b ↔ ∀ ε, 1 < ε → a < b * ε :=
+⟨λ h ε, lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul'⟩
+
+end has_exists_mul_of_le
+
 /-- A linearly ordered additive commutative monoid. -/
 @[protect_proj, ancestor linear_order ordered_add_comm_monoid]
 class linear_ordered_add_comm_monoid (α : Type*)

src/algebra/order/nonneg.lean

@@ -202,6 +202,9 @@ by apply_instance
 instance comm_monoid_with_zero [ordered_comm_semiring α] : comm_monoid_with_zero {x : α // 0 ≤ x} :=
 by apply_instance
 
+instance semiring [ordered_semiring α] : semiring {x : α // 0 ≤ x} := infer_instance
+instance comm_semiring [ordered_comm_semiring α] : comm_semiring {x : α // 0 ≤ x} := infer_instance
+
 instance nontrivial [linear_ordered_semiring α] : nontrivial {x : α // 0 ≤ x} :=
 ⟨ ⟨0, 1, λ h, zero_ne_one (congr_arg subtype.val h)⟩ ⟩
 

src/data/nat/choose/bounds.lean

@@ -23,7 +23,7 @@ bounds `n^r/r^r ≤ n.choose r ≤ e^r n^r/r^r` in the future.
 
 open_locale nat
 
-variables {α : Type*} [linear_ordered_field α]
+variables {α : Type*} [linear_ordered_semifield α]
 
 namespace nat
 

src/data/real/nnreal.lean

@@ -46,20 +46,16 @@ of `x` with `↑x`. This tactic also works for a function `f : α → ℝ` with
 ## Notations
 
 This file defines `ℝ≥0` as a localized notation for `nnreal`.
-
-## TODO
-
-`semifield` instance
 -/
 
 open_locale classical big_operators
 
 /-- Nonnegative real numbers. -/
 @[derive [
   ordered_semiring, comm_monoid_with_zero, -- to ensure these instance are computable
-  floor_semiring,
+  floor_semiring, comm_semiring, semiring,
   semilattice_inf, densely_ordered, order_bot,
-  canonically_linear_ordered_add_monoid, linear_ordered_comm_group_with_zero, archimedean,
+  canonically_linear_ordered_semifield, linear_ordered_comm_group_with_zero, archimedean,
   linear_ordered_semiring, ordered_comm_semiring, canonically_ordered_comm_semiring,
   has_sub, has_ordered_sub, has_div, inhabited]]
 def nnreal := {r : ℝ // 0 ≤ r}
@@ -130,7 +126,6 @@ protected lemma coe_two : ((2 : ℝ≥0) : ℝ) = 2 := rfl
   ((r₁ - r₂ : ℝ≥0) : ℝ) = r₁ - r₂ :=
 max_eq_left $ le_sub.2 $ by simp [show (r₂ : ℝ) ≤ r₁, from h]
 
--- TODO: setup semifield!
 @[simp, norm_cast] protected lemma coe_eq_zero (r : ℝ≥0) : ↑r = (0 : ℝ) ↔ r = 0 :=
 by rw [← nnreal.coe_zero, nnreal.coe_eq]
 
@@ -354,12 +349,9 @@ ordered_cancel_add_comm_monoid.to_contravariant_class_left ℝ≥0
 instance covariant_mul : covariant_class ℝ≥0 ℝ≥0 (*) (≤) :=
 ordered_comm_monoid.to_covariant_class_left ℝ≥0
 
+-- Why isn't `nnreal.contravariant_add` inferred?
 lemma le_of_forall_pos_le_add {a b : ℝ≥0} (h : ∀ε, 0 < ε → a ≤ b + ε) : a ≤ b :=
-le_of_forall_le_of_dense $ assume x hxb,
-begin
-  rcases exists_add_of_le (le_of_lt hxb) with ⟨ε, rfl⟩,
-  exact h _ ((lt_add_iff_pos_right b).1 hxb)
-end
+@le_of_forall_pos_le_add _ _ _ _ _ _ nnreal.contravariant_add _ _ h
 
 lemma lt_iff_exists_rat_btwn (a b : ℝ≥0) :
   a < b ↔ (∃q:ℚ, 0 ≤ q ∧ a < real.to_nnreal q ∧ real.to_nnreal q < b) :=
@@ -502,11 +494,7 @@ namespace nnreal
 section mul
 
 lemma mul_eq_mul_left {a b c : ℝ≥0} (h : a ≠ 0) : (a * b = a * c ↔ b = c) :=
-begin
-  rw [← nnreal.eq_iff, ← nnreal.eq_iff, nnreal.coe_mul, nnreal.coe_mul], split,
-  { exact mul_left_cancel₀ (mt (@nnreal.eq_iff a 0).1 h) },
-  { assume h, rw [h] }
-end
+by rw [mul_eq_mul_left_iff, or_iff_left h]
 
 lemma _root_.real.to_nnreal_mul {p q : ℝ} (hp : 0 ≤ p) :
   real.to_nnreal (p * q) = real.to_nnreal p * real.to_nnreal q :=
@@ -566,24 +554,21 @@ lemma coe_sub_def {r p : ℝ≥0} : ↑(r - p) = max (r - p : ℝ) 0 := rfl
 
 noncomputable example : has_ordered_sub ℝ≥0 := by apply_instance
 
-lemma sub_div (a b c : ℝ≥0) : (a - b) / c = a / c - b / c :=
-by simp only [div_eq_mul_inv, tsub_mul]
+lemma sub_div (a b c : ℝ≥0) : (a - b) / c = a / c - b / c := tsub_div _ _ _
 
 end sub
 
 section inv
 
 lemma sum_div {ι} (s : finset ι) (f : ι → ℝ≥0) (b : ℝ≥0) :
   (∑ i in s, f i) / b = ∑ i in s, (f i / b) :=
-by simp only [div_eq_mul_inv, finset.sum_mul]
+finset.sum_div
 
-@[simp] lemma inv_pos {r : ℝ≥0} : 0 < r⁻¹ ↔ 0 < r :=
-by simp [pos_iff_ne_zero]
+@[simp] lemma inv_pos {r : ℝ≥0} : 0 < r⁻¹ ↔ 0 < r := inv_pos
 
-lemma div_pos {r p : ℝ≥0} (hr : 0 < r) (hp : 0 < p) : 0 < r / p :=
-by simpa only [div_eq_mul_inv] using mul_pos hr (inv_pos.2 hp)
+lemma div_pos {r p : ℝ≥0} (hr : 0 < r) (hp : 0 < p) : 0 < r / p := div_pos hr hp
 
-lemma div_self_le (r : ℝ≥0) : r / r ≤ 1 := div_self_le_one (r : ℝ)
+lemma div_self_le (r : ℝ≥0) : r / r ≤ 1 := div_self_le_one r
 
 @[simp] lemma inv_le {r p : ℝ≥0} (h : r ≠ 0) : r⁻¹ ≤ p ↔ 1 ≤ r * p :=
 by rw [← mul_le_mul_left (pos_iff_ne_zero.2 h), mul_inv_cancel h]
@@ -601,11 +586,9 @@ lemma mul_le_iff_le_inv {a b r : ℝ≥0} (hr : r ≠ 0) : r * a ≤ b ↔ a ≤
 have 0 < r, from lt_of_le_of_ne (zero_le r) hr.symm,
 by rw [← mul_le_mul_left (inv_pos.mpr this), ← mul_assoc, inv_mul_cancel hr, one_mul]
 
-lemma le_div_iff_mul_le {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b :=
-by rw [div_eq_inv_mul, ← mul_le_iff_le_inv hr, mul_comm]
+lemma le_div_iff_mul_le {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b := le_div_iff₀ hr
 
-lemma div_le_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ b * r :=
-@div_le_iff ℝ _ a r b $ pos_iff_ne_zero.2 hr
+lemma div_le_iff {a b r : ℝ≥0} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ b * r := div_le_iff₀ hr
 
 lemma div_le_iff' {a b r : ℝ≥0} (hr : r ≠ 0) : a / r ≤ b ↔ a ≤ r * b :=
 @div_le_iff' ℝ _ a r b $ pos_iff_ne_zero.2 hr
@@ -653,8 +636,7 @@ end
 
 lemma div_le_div_left {a b c : ℝ≥0} (a0 : 0 < a) (b0 : 0 < b) (c0 : 0 < c) :
   a / b ≤ a / c ↔ c ≤ b :=
-by rw [nnreal.div_le_iff b0.ne.symm, div_mul_eq_mul_div, nnreal.le_div_iff_mul_le c0.ne.symm,
-  mul_le_mul_left a0]
+div_le_div_left a0 b0 c0
 
 lemma le_of_forall_lt_one_mul_le {x y : ℝ≥0} (h : ∀a<1, a * x ≤ y) : x ≤ y :=
 le_of_forall_ge_of_dense $ assume a ha,
@@ -664,21 +646,17 @@ le_of_forall_ge_of_dense $ assume a ha,
   have (a * x⁻¹) * x ≤ y, from h _ this,
   by rwa [mul_assoc, inv_mul_cancel hx, mul_one] at this
 
-lemma div_add_div_same (a b c : ℝ≥0) : a / c + b / c = (a + b) / c :=
-eq.symm $ right_distrib a b (c⁻¹)
+lemma div_add_div_same (a b c : ℝ≥0) : a / c + b / c = (a + b) / c := div_add_div_same _ _ _
 
-lemma half_pos {a : ℝ≥0} (h : 0 < a) : 0 < a / 2 := div_pos h zero_lt_two
+lemma half_pos {a : ℝ≥0} (h : 0 < a) : 0 < a / 2 := half_pos h
 
-lemma add_halves (a : ℝ≥0) : a / 2 + a / 2 = a := nnreal.eq (add_halves a)
+lemma add_halves (a : ℝ≥0) : a / 2 + a / 2 = a := add_halves _
 
-lemma half_le_self (a : ℝ≥0) : a / 2 ≤ a := nnreal.coe_le_coe.mp $ half_le_self a.coe_nonneg
+lemma half_le_self (a : ℝ≥0) : a / 2 ≤ a := half_le_self bot_le
 
-lemma half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a :=
-by rw [← nnreal.coe_lt_coe, nnreal.coe_div]; exact
-half_lt_self (bot_lt_iff_ne_bot.2 h)
+lemma half_lt_self {a : ℝ≥0} (h : a ≠ 0) : a / 2 < a := half_lt_self h.bot_lt
 
-lemma two_inv_lt_one : (2⁻¹:ℝ≥0) < 1 :=
-by simpa using half_lt_self zero_ne_one.symm
+lemma two_inv_lt_one : (2⁻¹:ℝ≥0) < 1 := two_inv_lt_one
 
 lemma div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1 :=
 begin
@@ -688,19 +666,15 @@ end
 
 @[field_simps] lemma div_add_div (a : ℝ≥0) {b : ℝ≥0} (c : ℝ≥0) {d : ℝ≥0}
   (hb : b ≠ 0) (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d) :=
-begin
-  rw ← nnreal.eq_iff,
-  simp only [nnreal.coe_add, nnreal.coe_div, nnreal.coe_mul],
-  exact div_add_div _ _ (coe_ne_zero.2 hb) (coe_ne_zero.2 hd)
-end
+div_add_div _ _ hb hd
 
 @[field_simps] lemma add_div' (a b c : ℝ≥0) (hc : c ≠ 0) :
   b + a / c = (b * c + a) / c :=
-by simpa using div_add_div b a one_ne_zero hc
+add_div' _ _ _ hc
 
 @[field_simps] lemma div_add' (a b c : ℝ≥0) (hc : c ≠ 0) :
   a / c + b = (a + b * c) / c :=
-by rwa [add_comm, add_div', add_comm]
+div_add' _ _ _ hc
 
 lemma _root_.real.to_nnreal_inv {x : ℝ} :
   real.to_nnreal x⁻¹ = (real.to_nnreal x)⁻¹ :=
@@ -723,8 +697,7 @@ by rw [div_eq_inv_mul, div_eq_inv_mul, real.to_nnreal_mul (inv_nonneg.2 hy), rea
 lemma inv_lt_one_iff {x : ℝ≥0} (hx : x ≠ 0) : x⁻¹ < 1 ↔ 1 < x :=
 by rwa [← one_div, div_lt_iff hx, one_mul]
 
-lemma inv_lt_one {x : ℝ≥0} (hx : 1 < x) : x⁻¹ < 1 :=
-(inv_lt_one_iff (zero_lt_one.trans hx).ne').2 hx
+lemma inv_lt_one {x : ℝ≥0} (hx : 1 < x) : x⁻¹ < 1 := inv_lt_one hx
 
 lemma zpow_pos {x : ℝ≥0} (hx : x ≠ 0) (n : ℤ) : 0 < x ^ n :=
 begin
@@ -733,9 +706,7 @@ begin
   { simp [pow_pos hx.bot_lt _] }
 end
 
-lemma inv_lt_inv_iff {x y : ℝ≥0} (hx : x ≠ 0) (hy : y ≠ 0) :
-  y⁻¹ < x⁻¹ ↔ x < y :=
-by rw [← one_div, div_lt_iff hy, ← div_eq_inv_mul, lt_div_iff hx, one_mul]
+lemma inv_lt_inv_iff {x y : ℝ≥0} (hx : x ≠ 0) (hy : y ≠ 0) : y⁻¹ < x⁻¹ ↔ x < y := inv_lt_inv₀ hy hx
 
 lemma inv_lt_inv {x y : ℝ≥0} (hx : x ≠ 0) (h : x < y) : y⁻¹ < x⁻¹ :=
 (inv_lt_inv_iff hx ((bot_le.trans_lt h).ne')).2 h

src/order/filter/at_top_bot.lean

@@ -788,9 +788,9 @@ lemma nonneg_of_eventually_pow_nonneg [linear_ordered_ring α] {a : α}
   (h : ∀ᶠ n in at_top, 0 ≤ a ^ (n : ℕ)) : 0 ≤ a :=
 let ⟨n, hn⟩ := (tendsto_bit1_at_top.eventually h).exists in pow_bit1_nonneg_iff.1 hn
 
-section linear_ordered_field
+section linear_ordered_semifield
 
-variables [linear_ordered_field α] {l : filter β} {f : β → α} {r : α}
+variables [linear_ordered_semifield α] {l : filter β} {f : β → α} {r c : α} {n : ℕ}
 
 /-- If a function tends to infinity along a filter, then this function multiplied by a positive
 constant (on the left) also tends to infinity. For a version working in `ℕ` or `ℤ`, use
@@ -812,6 +812,25 @@ lemma tendsto.at_top_div_const (hr : 0 < r) (hf : tendsto f l at_top) :
   tendsto (λx, f x / r) l at_top :=
 by simpa only [div_eq_mul_inv] using hf.at_top_mul_const (inv_pos.2 hr)
 
+lemma tendsto_const_mul_pow_at_top (hn : n ≠ 0) (hc : 0 < c) :
+  tendsto (λ x, c * x^n) at_top at_top :=
+tendsto.const_mul_at_top hc (tendsto_pow_at_top hn)
+
+lemma tendsto_const_mul_pow_at_top_iff  :
+  tendsto (λ x, c * x^n) at_top at_top ↔ n ≠ 0 ∧ 0 < c :=
+begin
+  refine ⟨λ h, ⟨_, _⟩, λ h, tendsto_const_mul_pow_at_top h.1 h.2⟩,
+  { rintro rfl,
+    simpa only [pow_zero, not_tendsto_const_at_top] using h },
+  { rcases ((h.eventually_gt_at_top 0).and (eventually_ge_at_top 0)).exists with ⟨k, hck, hk⟩,
+    exact pos_of_mul_pos_left hck (pow_nonneg hk _) },
+end
+
+end linear_ordered_semifield
+
+section linear_ordered_field
+variables [linear_ordered_field α] {l : filter β} {f : β → α} {r : α}
+
 /-- If a function tends to infinity along a filter, then this function multiplied by a negative
 constant (on the left) tends to negative infinity. -/
 lemma tendsto.neg_const_mul_at_top (hr : r < 0) (hf : tendsto f l at_top) :
@@ -857,20 +876,6 @@ lemma tendsto.at_bot_mul_neg_const (hr : r < 0) (hf : tendsto f l at_bot) :
   tendsto (λ x, f x * r) l at_top :=
 by simpa only [mul_comm] using hf.neg_const_mul_at_bot hr
 
-lemma tendsto_const_mul_pow_at_top {c : α} {n : ℕ}
-  (hn : n ≠ 0) (hc : 0 < c) : tendsto (λ x, c * x^n) at_top at_top :=
-tendsto.const_mul_at_top hc (tendsto_pow_at_top hn)
-
-lemma tendsto_const_mul_pow_at_top_iff {c : α} {n : ℕ} :
-  tendsto (λ x, c * x^n) at_top at_top ↔ n ≠ 0 ∧ 0 < c :=
-begin
-  refine ⟨λ h, ⟨_, _⟩, λ h, tendsto_const_mul_pow_at_top h.1 h.2⟩,
-  { rintro rfl,
-    simpa only [pow_zero, not_tendsto_const_at_top] using h },
-  { rcases ((h.eventually_gt_at_top 0).and (eventually_ge_at_top 0)).exists with ⟨k, hck, hk⟩,
-    exact pos_of_mul_pos_left hck (pow_nonneg hk _) },
-end
-
 lemma tendsto_neg_const_mul_pow_at_top {c : α} {n : ℕ}
   (hn : n ≠ 0) (hc : c < 0) : tendsto (λ x, c * x^n) at_top at_bot :=
 tendsto.neg_const_mul_at_top hc (tendsto_pow_at_top hn)