chore(algebra/ordered_field): merge inv_pos / zero_lt_inv with inv_pos' / inv_neg (#2226)

* chore(algebra/ordered_field): merge `inv_pos` / `zero_lt_inv` with `inv_pos'` / `inv_neg`

Also move some lemmas to `linear_ordered_field`

* Update src/data/real/hyperreal.lean

* Fix compile

* Actually fix compile of `data/real/hyperreal`

Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: 3 people

src/algebra/archimedean.lean

@@ -81,7 +81,7 @@ by classical; exact
 let ⟨N, hN⟩ := pow_unbounded_of_one_lt x⁻¹ hy in
   have he: ∃ m : ℤ, y ^ m ≤ x, from
     ⟨-N, le_of_lt (by rw [(fpow_neg y (↑N)), one_div_eq_inv];
-    exact (inv_lt hx (lt_trans (inv_pos hx) hN)).1 hN)⟩,
+    exact (inv_lt hx (lt_trans (inv_pos.2 hx) hN)).1 hN)⟩,
 let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy in
   have hb: ∃ b : ℤ, ∀ m, y ^ m ≤ x → m ≤ b, from
     ⟨M, λ m hm, le_of_not_lt (λ hlt, not_lt_of_ge
@@ -95,7 +95,7 @@ but with ≤ and < the other way around. -/
 lemma exists_int_pow_near' [discrete_linear_ordered_field α] [archimedean α]
   {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
   ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) :=
-let ⟨m, hle, hlt⟩ := exists_int_pow_near (inv_pos hx) hy in
+let ⟨m, hle, hlt⟩ := exists_int_pow_near (inv_pos.2 hx) hy in
 have hyp : 0 < y, from lt_trans (discrete_linear_ordered_field.zero_lt_one α) hy,
 ⟨-(m+1),
 by rwa [fpow_neg, one_div_eq_inv, inv_lt (fpow_pos_of_pos hyp _) hx],
@@ -180,7 +180,7 @@ begin
   cases exists_nat_gt (y - x)⁻¹ with n nh,
   cases exists_floor (x * n) with z zh,
   refine ⟨(z + 1 : ℤ) / n, _⟩,
-  have n0 := nat.cast_pos.1 (lt_trans (inv_pos (sub_pos.2 h)) nh),
+  have n0 := nat.cast_pos.1 (lt_trans (inv_pos.2 (sub_pos.2 h)) nh),
   have n0' := (@nat.cast_pos α _ _).2 n0,
   rw [rat.cast_div_of_ne_zero, rat.cast_coe_nat, rat.cast_coe_int, div_lt_iff n0'],
   refine ⟨(lt_div_iff n0').2 $

src/algebra/ordered_field.lean

@@ -10,11 +10,21 @@ variables {α : Type*} [linear_ordered_field α] {a b c d : α}
 
 lemma div_pos : 0 < a → 0 < b → 0 < a / b := div_pos_of_pos_of_pos
 
-lemma inv_pos {a : α} : 0 < a → 0 < a⁻¹ :=
-by rw [inv_eq_one_div]; exact div_pos zero_lt_one
+@[simp] lemma inv_pos : ∀ {a : α}, 0 < a⁻¹ ↔ 0 < a :=
+suffices ∀ a : α, 0 < a → 0 < a⁻¹,
+from λ a, ⟨λ h, inv_inv'' a ▸ this _ h, this a⟩,
+λ a, one_div_eq_inv a ▸ one_div_pos_of_pos
 
-lemma inv_lt_zero {a : α} : a < 0 → a⁻¹ < 0 :=
-by rw [inv_eq_one_div]; exact div_neg_of_pos_of_neg zero_lt_one
+@[simp] lemma inv_lt_zero : ∀ {a : α}, a⁻¹ < 0 ↔ a < 0 :=
+suffices ∀ a : α, a < 0 → a⁻¹ < 0,
+from λ a, ⟨λ h, inv_inv'' a ▸ this _ h, this a⟩,
+λ a, one_div_eq_inv a ▸ one_div_neg_of_neg
+
+@[simp] lemma inv_nonneg {a : α} : 0 ≤ a⁻¹ ↔ 0 ≤ a :=
+le_iff_le_iff_lt_iff_lt.2 inv_lt_zero
+
+@[simp] lemma inv_nonpos {a : α} : a⁻¹ ≤ 0 ↔ a ≤ 0 :=
+le_iff_le_iff_lt_iff_lt.2 inv_pos
 
 lemma one_le_div_iff_le (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a :=
 ⟨le_of_one_le_div a hb, one_le_div_of_le a hb⟩
@@ -67,10 +77,10 @@ by rw [inv_eq_one_div, div_le_iff ha,
        ← div_eq_inv_mul, one_le_div_iff_le hb]
 
 lemma inv_le (ha : 0 < a) (hb : 0 < b) : a⁻¹ ≤ b ↔ b⁻¹ ≤ a :=
-by rw [← inv_le_inv hb (inv_pos ha), inv_inv']
+by rw [← inv_le_inv hb (inv_pos.2 ha), inv_inv']
 
 lemma le_inv (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
-by rw [← inv_le_inv (inv_pos hb) ha, inv_inv']
+by rw [← inv_le_inv (inv_pos.2 hb) ha, inv_inv']
 
 lemma one_div_le_one_div (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ 1 / b ↔ b ≤ a :=
 by simpa [one_div_eq_inv] using inv_le_inv ha hb
@@ -174,14 +184,31 @@ by haveI := classical.dec_eq α; exact
 if ha0 : a = 0 then by simp [ha0]
 else (div_le_div_left (lt_of_le_of_ne ha (ne.symm ha0)) (lt_of_lt_of_le hc h) hc).2 h
 
+lemma inv_neg : (-a)⁻¹ = -(a⁻¹) :=
+by rwa [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
+
+lemma inv_le_inv_of_le {a b : α} (hb : 0 < b) (h : b ≤ a) : a⁻¹ ≤ b⁻¹ :=
+begin
+  rw [inv_eq_one_div, inv_eq_one_div],
+  exact one_div_le_one_div_of_le hb h
+end
+
+lemma div_nonneg' {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b :=
+(lt_or_eq_of_le hb).elim (div_nonneg ha) (λ h, by simp [h.symm])
+
+lemma div_le_div_of_le_of_nonneg {a b c : α} (hab : a ≤ b) (hc : 0 ≤ c) :
+  a / c ≤ b / c :=
+mul_le_mul_of_nonneg_right hab (inv_nonneg.2 hc)
+
+
 end linear_ordered_field
 
 namespace nat
 
 variables {α : Type*} [linear_ordered_field α]
 
 lemma inv_pos_of_nat {n : ℕ} : 0 < ((n : α) + 1)⁻¹ :=
-inv_pos $ add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one
+inv_pos.2 $ add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one
 
 lemma one_div_pos_of_nat {n : ℕ} : 0 < 1 / ((n : α) + 1) :=
 by { rw one_div_eq_inv, exact inv_pos_of_nat }
@@ -197,37 +224,9 @@ end nat
 section
 variables {α : Type*} [discrete_linear_ordered_field α] (a b c : α)
 
-@[simp] lemma inv_pos' {a : α} : 0 < a⁻¹ ↔ 0 < a :=
-⟨by rw [inv_eq_one_div]; exact pos_of_one_div_pos, inv_pos⟩
-
-@[simp] lemma inv_neg' {a : α} : a⁻¹ < 0 ↔ a < 0 :=
-⟨by rw [inv_eq_one_div]; exact neg_of_one_div_neg, inv_lt_zero⟩
-
-@[simp] lemma inv_nonneg {a : α} : 0 ≤ a⁻¹ ↔ 0 ≤ a :=
-le_iff_le_iff_lt_iff_lt.2 inv_neg'
-
-@[simp] lemma inv_nonpos {a : α} : a⁻¹ ≤ 0 ↔ a ≤ 0 :=
-le_iff_le_iff_lt_iff_lt.2 inv_pos'
-
 lemma abs_inv : abs a⁻¹ = (abs a)⁻¹ :=
 have h : abs (1 / a) = 1 / abs a,
   begin rw [abs_div, abs_of_nonneg], exact zero_le_one end,
 by simp [*] at *
 
-lemma inv_neg : (-a)⁻¹ = -(a⁻¹) :=
-by rwa [inv_eq_one_div, inv_eq_one_div, div_neg_eq_neg_div]
-
-lemma inv_le_inv_of_le {a b : α} (hb : 0 < b) (h : b ≤ a) : a⁻¹ ≤ b⁻¹ :=
-begin
-  rw [inv_eq_one_div, inv_eq_one_div],
-  exact one_div_le_one_div_of_le hb h
-end
-
-lemma div_nonneg' {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b :=
-(lt_or_eq_of_le hb).elim (div_nonneg ha) (λ h, by simp [h.symm])
-
-lemma div_le_div_of_le_of_nonneg {a b c : α} (hab : a ≤ b) (hc : 0 ≤ c) :
-  a / c ≤ b / c :=
-mul_le_mul_of_nonneg_right hab (inv_nonneg.2 hc)
-
 end

src/analysis/calculus/mean_value.lean

@@ -115,7 +115,7 @@ begin
         (Ioc_mem_nhds_within_Ioi ⟨le_refl _, hy⟩)).exists,
     have := le_of_lt (lt_trans hfz hzB),
     refine ⟨z, _, hz⟩,
-    rw [mul_le_mul_left (inv_pos $ sub_pos.2 hz.1), hxB, sub_le_sub_iff_right] at this,
+    rw [mul_le_mul_left (inv_pos.2 $ sub_pos.2 hz.1), hxB, sub_le_sub_iff_right] at this,
     exact this }
 end
 

src/analysis/calculus/tangent_cone.lean

@@ -157,7 +157,7 @@ begin
         rw [← mul_assoc, mul_inv_cancel, one_mul],
         exact ne_of_gt c_pos
       end },
-    { apply mul_pos (inv_pos c_pos) (pow_pos _ _),
+    { apply mul_pos (inv_pos.2 c_pos) (pow_pos _ _),
       norm_num } },
   choose d' hd' using this,
   refine ⟨c, λn, (d n, d' n), _, hc, _⟩,
@@ -197,7 +197,7 @@ begin
         rw [← mul_assoc, mul_inv_cancel, one_mul],
         exact ne_of_gt c_pos
       end },
-    { apply mul_pos (inv_pos c_pos) (pow_pos _ _),
+    { apply mul_pos (inv_pos.2 c_pos) (pow_pos _ _),
       norm_num } },
   choose d' hd' using this,
   refine ⟨c, λn, (d' n, d n), _, hc, _⟩,

src/analysis/complex/exponential.lean

@@ -342,13 +342,13 @@ continuous_iff_continuous_at.2 $ λ x,
 begin
   rw continuous_at,
   let f₁ := λ h:{h:ℝ // 0 < h}, log (x.1 * h.1),
-  let f₂ := λ y:{y:ℝ // 0 < y}, subtype.mk (x.1 ⁻¹ * y.1) (mul_pos (inv_pos x.2) y.2),
+  let f₂ := λ y:{y:ℝ // 0 < y}, subtype.mk (x.1 ⁻¹ * y.1) (mul_pos (inv_pos.2 x.2) y.2),
   have H1 : tendsto f₁ (𝓝 ⟨1, zero_lt_one⟩) (𝓝 (log (x.1*1))),
     have : f₁ = λ h:{h:ℝ // 0 < h}, log x.1 + log h.1,
       ext h, rw ← log_mul x.2 h.2,
     simp only [this, log_mul x.2 zero_lt_one, log_one],
     exact tendsto_const_nhds.add (tendsto.comp tendsto_log_one_zero continuous_at_subtype_val),
-  have H2 : tendsto f₂ (𝓝 x) (𝓝 ⟨x.1⁻¹ * x.1, mul_pos (inv_pos x.2) x.2⟩),
+  have H2 : tendsto f₂ (𝓝 x) (𝓝 ⟨x.1⁻¹ * x.1, mul_pos (inv_pos.2 x.2) x.2⟩),
     rw tendsto_subtype_rng, exact tendsto_const_nhds.mul continuous_at_subtype_val,
   suffices h : tendsto (f₁ ∘ f₂) (𝓝 x) (𝓝 (log x.1)),
   begin

src/analysis/convex/basic.lean

@@ -162,9 +162,9 @@ lemma convex_iff_div:
 ⟨begin
   assume h x y hx hy a b ha hb hab,
   apply h hx hy,
-  have ha', from mul_le_mul_of_nonneg_left ha (le_of_lt (inv_pos hab)),
+  have ha', from mul_le_mul_of_nonneg_left ha (le_of_lt (inv_pos.2 hab)),
   rwa [mul_zero, ←div_eq_inv_mul] at ha',
-  have hb', from mul_le_mul_of_nonneg_left hb (le_of_lt (inv_pos hab)),
+  have hb', from mul_le_mul_of_nonneg_left hb (le_of_lt (inv_pos.2 hab)),
   rwa [mul_zero, ←div_eq_inv_mul] at hb',
   rw [←add_div],
   exact div_self (ne_of_lt hab).symm

src/analysis/convex/cone.lean

@@ -100,7 +100,7 @@ lemma add_mem ⦃x⦄ (hx : x ∈ S) ⦃y⦄ (hy : y ∈ S) : x + y ∈ S := S.a
 lemma smul_mem_iff {c : ℝ} (hc : 0 < c) {x : E} :
   c • x ∈ S ↔ x ∈ S :=
 ⟨λ h, by simpa only [smul_smul, inv_mul_cancel (ne_of_gt hc), one_smul]
-  using S.smul_mem (inv_pos hc) h, λ h, S.smul_mem hc h⟩
+  using S.smul_mem (inv_pos.2 hc) h, λ h, S.smul_mem hc h⟩
 
 lemma convex : convex (S : set E) :=
 convex_iff_forall_pos.2 $ λ x y hx hy a b ha hb hab,
@@ -217,9 +217,9 @@ lemma mem_to_cone' : x ∈ hs.to_cone s ↔ ∃ c > 0, (c : ℝ) • x ∈ s :=
 begin
   refine hs.mem_to_cone.trans ⟨_, _⟩,
   { rintros ⟨c, hc, y, hy, rfl⟩,
-    exact ⟨c⁻¹, inv_pos hc, by rwa [smul_smul, inv_mul_cancel (ne_of_gt hc), one_smul]⟩ },
+    exact ⟨c⁻¹, inv_pos.2 hc, by rwa [smul_smul, inv_mul_cancel (ne_of_gt hc), one_smul]⟩ },
   { rintros ⟨c, hc, hcx⟩,
-    exact ⟨c⁻¹, inv_pos hc, _, hcx, by rw [smul_smul, inv_mul_cancel (ne_of_gt hc), one_smul]⟩ }
+    exact ⟨c⁻¹, inv_pos.2 hc, _, hcx, by rw [smul_smul, inv_mul_cancel (ne_of_gt hc), one_smul]⟩ }
 end
 
 lemma subset_to_cone : s ⊆ hs.to_cone s :=

src/analysis/normed_space/multilinear.lean

@@ -105,7 +105,7 @@ begin
   set C := (1 + ∥f 0∥) * univ.prod (λ(i : ι), δ⁻¹ * ∥c∥),
   have C_pos : 0 < C :=
     mul_pos (lt_of_lt_of_le zero_lt_one (by simp))
-      (prod_pos (λi hi, mul_pos (inv_pos δ_pos) (lt_of_le_of_lt zero_le_one hc))),
+      (prod_pos (λi hi, mul_pos (inv_pos.2 δ_pos) (lt_of_le_of_lt zero_le_one hc))),
   refine ⟨C, C_pos, λm, _⟩,
   /- Given a general point `m`, rescale each coordinate to bring it to `[δ/∥c∥, δ]` by multiplication
   by a power of a scalar `c` with norm `∥c∥ > 1`.-/

src/analysis/normed_space/operator_norm.lean

@@ -155,7 +155,7 @@ begin
       exact lt_of_le_of_lt ha (half_lt_self ε_pos) },
     simpa using this },
   rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
-  refine ⟨δ⁻¹ * ∥c∥, mul_pos (inv_pos δ_pos) (lt_trans zero_lt_one hc), (λx, _)⟩,
+  refine ⟨δ⁻¹ * ∥c∥, mul_pos (inv_pos.2 δ_pos) (lt_trans zero_lt_one hc), (λx, _)⟩,
   by_cases h : x = 0,
   { simp only [h, norm_zero, mul_zero, linear_map.map_zero] },
   { rcases rescale_to_shell hc δ_pos h with ⟨d, hd, dxle, ledx, dinv⟩,

src/analysis/specific_limits.lean

@@ -82,7 +82,7 @@ constant also tends to infinity. -/
 lemma tendsto_at_top_div [linear_ordered_field α]
   {l : filter β} {r : α} (hr : 0 < r) {f : β → α} (hf : tendsto f l at_top) :
   tendsto (λx, f x / r) l at_top :=
-tendsto_at_top_mul_right' (inv_pos hr) hf
+tendsto_at_top_mul_right' (inv_pos.2 hr) hf
 
 /-- The function `x ↦ x⁻¹` tends to `+∞` on the right of `0`. -/
 lemma tendsto_inv_zero_at_top [discrete_linear_ordered_field α] [topological_space α]
@@ -106,8 +106,8 @@ begin
   rcases hs with ⟨C, C0, hC⟩,
   change 0 < C at C0,
   refine filter.mem_map.2 (mem_sets_of_superset (mem_at_top C⁻¹) (λ x hx, hC _)),
-  have : 0 < x, from lt_of_lt_of_le (inv_pos C0) hx,
-  exact ⟨inv_pos this, (inv_le C0 this).1 hx⟩
+  have : 0 < x, from lt_of_lt_of_le (inv_pos.2 C0) hx,
+  exact ⟨inv_pos.2 this, (inv_le C0 this).1 hx⟩
 end
 
 lemma tendsto_inv_at_top_zero [discrete_linear_ordered_field α] [topological_space α]