fix(algebra/field) remove one_div_eq_inv (#3749)

fpvandoorn · fpvandoorn · commit 6c8b2cd61361 · 2020-08-13T06:22:20.000Z
It already existed as `one_div` for `group_with_zero`
Also make `one_div` a `simp` lemma and renamed `nnreal.one_div_eq_inv` to `nnreal.one_div`.
diff --git a/src/algebra/archimedean.lean b/src/algebra/archimedean.lean
@@ -194,7 +194,7 @@ begin
   rw [int.cast_add, int.cast_one],
   refine lt_of_le_of_lt (add_le_add_right ((zh _).1 (le_refl _)) _) _,
   rwa [← lt_sub_iff_add_lt', ← sub_mul,
-       ← div_lt_iff' (sub_pos.2 h), one_div_eq_inv],
+       ← div_lt_iff' (sub_pos.2 h), one_div],
   { rw [rat.coe_int_denom, nat.cast_one], exact one_ne_zero },
   { intro H, rw [rat.coe_nat_num, ← coe_coe, nat.cast_eq_zero] at H, subst H, cases n0 },
   { rw [rat.coe_nat_denom, nat.cast_one], exact one_ne_zero }
diff --git a/src/algebra/field.lean b/src/algebra/field.lean
@@ -32,8 +32,6 @@ instance division_ring.to_group_with_zero :
 { .. ‹division_ring α›,
   .. (infer_instance : semiring α) }
 
-@[simp] lemma one_div_eq_inv (a : α) : 1 / a = a⁻¹ := one_mul a⁻¹
-
 @[field_simps] lemma inv_eq_one_div (a : α) : a⁻¹ = 1 / a := by simp
 
 local attribute [simp]
diff --git a/src/algebra/field_power.lean b/src/algebra/field_power.lean
@@ -37,7 +37,7 @@ begin
   { apply absurd h,
     apply not_le_of_gt,
     exact lt_of_lt_of_le (neg_succ_lt_zero _) (of_nat_nonneg _) },
-  { simp only [fpow_neg_succ_of_nat, one_div_eq_inv],
+  { simp only [fpow_neg_succ_of_nat, one_div],
     apply le_trans (inv_le_one _); apply one_le_pow_of_one_le hx },
   { simp only [fpow_neg_succ_of_nat],
     apply (inv_le_inv _ _).2,
diff --git a/src/algebra/group_with_zero.lean b/src/algebra/group_with_zero.lean
@@ -584,7 +584,7 @@ end
 
 @[simp] lemma div_one (a : G₀) : a / 1 = a := by simp [div_eq_mul_inv]
 
-lemma one_div (a : G₀) : 1 / a = a⁻¹ := one_mul _
+@[simp] lemma one_div (a : G₀) : 1 / a = a⁻¹ := one_mul _
 
 @[simp] lemma zero_div (a : G₀) : 0 / a = 0 := zero_mul _
 
@@ -632,7 +632,7 @@ by simpa only [one_div] using eq_inv_of_mul_left_eq_one h
 @[simp] lemma one_div_div (a b : G₀) : 1 / (a / b) = b / a :=
 by rw [one_div, div_eq_mul_inv, mul_inv_rev', inv_inv', div_eq_mul_inv]
 
-@[simp] lemma one_div_one_div (a : G₀) : 1 / (1 / a) = a :=
+lemma one_div_one_div (a : G₀) : 1 / (1 / a) = a :=
 by simp
 
 lemma eq_of_one_div_eq_one_div {a b : G₀} (h : 1 / a = 1 / b) : a = b :=
diff --git a/src/algebra/ordered_field.lean b/src/algebra/ordered_field.lean
@@ -393,7 +393,7 @@ lemma le_inv (ha : 0 < a) (hb : 0 < b) : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
 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
+by simpa [one_div] using inv_le_inv ha hb
 
 lemma inv_lt_inv (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b⁻¹ ↔ b < a :=
 lt_iff_lt_of_le_iff_le (inv_le_inv hb ha)
@@ -402,7 +402,7 @@ lemma inv_lt (ha : 0 < a) (hb : 0 < b) : a⁻¹ < b ↔ b⁻¹ < a :=
 lt_iff_lt_of_le_iff_le (le_inv hb ha)
 
 lemma one_div_lt (ha : 0 < a) (hb : 0 < b) : 1 / a < b ↔ 1 / b < a :=
-(one_div_eq_inv a).symm ▸ (one_div_eq_inv b).symm ▸ inv_lt ha hb
+(one_div a).symm ▸ (one_div b).symm ▸ inv_lt ha hb
 
 lemma one_div_le (ha : 0 < a) (hb : 0 < b) : 1 / a ≤ b ↔ 1 / b ≤ a :=
 by simpa using inv_le ha hb
diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
@@ -96,7 +96,7 @@ begin
   have A : ∀ n : ℕ , 0 < n →
     (r : ennreal) ≤ ((C + 1)^(1/(n : ℝ)) : nnreal) * (1 / (nnnorm (p n) ^ (1/(n:ℝ)) : nnreal)),
   { assume n npos,
-    simp only [one_div_eq_inv, mul_assoc, mul_one, eq.symm ennreal.mul_div_assoc],
+    simp only [one_div, mul_assoc, mul_one, eq.symm ennreal.mul_div_assoc],
     rw [ennreal.le_div_iff_mul_le _ _, ← nnreal.pow_nat_rpow_nat_inv r npos, ← ennreal.coe_mul,
         ennreal.coe_le_coe, ← nnreal.mul_rpow, mul_comm],
     { exact nnreal.rpow_le_rpow (le_trans (h n) (le_add_right (le_refl _))) (by simp) },
@@ -137,7 +137,7 @@ begin
     rw [nnreal.lt_inv_iff_mul_lt A, mul_comm] at B,
     have : (nnnorm (p n) ^ (1 / (n : ℝ)) * r) ^ n ≤ 1 :=
       pow_le_one n (zero_le (nnnorm (p n) ^ (1 / ↑n) * r)) (le_of_lt B),
-    rw [mul_pow, one_div_eq_inv, nnreal.rpow_nat_inv_pow_nat _ (lt_of_le_of_lt (zero_le _) hn)]
+    rw [mul_pow, one_div, nnreal.rpow_nat_inv_pow_nat _ (lt_of_le_of_lt (zero_le _) hn)]
       at this,
     exact le_trans this (le_max_right _ _) },
 end
diff --git a/src/analysis/asymptotics.lean b/src/analysis/asymptotics.lean
@@ -1076,7 +1076,7 @@ theorem is_O_with.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c
 mem_sets_of_superset h $ λ x hx,
 begin
   simp only [mem_set_of_eq] at hx ⊢,
-  rw [mul_comm, one_div_eq_inv, ← div_eq_mul_inv, le_div_iff, mul_sub, mul_one, mul_comm],
+  rw [mul_comm, one_div, ← div_eq_mul_inv, le_div_iff, mul_sub, mul_one, mul_comm],
   { exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _) },
   { exact sub_pos.2 hc }
 end
diff --git a/src/analysis/calculus/deriv.lean b/src/analysis/calculus/deriv.lean
@@ -1630,7 +1630,7 @@ begin
   rcases lt_trichotomy m 0 with hm|hm|hm,
   { have := (has_strict_deriv_at_inv _).scomp _ (this (-m) (neg_pos.2 hm));
       [skip, exact fpow_ne_zero_of_ne_zero hx _],
-    simp only [(∘), fpow_neg, one_div_eq_inv, inv_inv', smul_eq_mul] at this,
+    simp only [(∘), fpow_neg, one_div, inv_inv', smul_eq_mul] at this,
     convert this using 1,
     rw [pow_two, mul_inv', inv_inv', int.cast_neg, ← neg_mul_eq_neg_mul, neg_mul_neg,
       ← fpow_add hx, mul_assoc, ← fpow_add hx], congr, abel },
diff --git a/src/analysis/convex/basic.lean b/src/analysis/convex/basic.lean
@@ -673,7 +673,7 @@ begin
   simp only [center_mass, sum_insert ha, smul_add, (mul_smul _ _ _).symm],
   congr' 2,
   { apply mul_comm },
-  { rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div_eq_inv] }
+  { rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div] }
 end
 
 lemma finset.center_mass_singleton (hw : w i ≠ 0) : ({i} : finset ι).center_mass w z = z i :=
diff --git a/src/analysis/mean_inequalities.lean b/src/analysis/mean_inequalities.lean
@@ -427,7 +427,7 @@ begin
     simp [this] },
   push_neg at H,
   by_cases H' : (∑ i in s, (f i)^p) ^ (1/p) = ⊤ ∨ (∑ i in s, (g i)^q) ^ (1/q) = ⊤,
-  { cases H'; simp [H', -one_div_eq_inv, H] },
+  { cases H'; simp [H', -one_div, H] },
   replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ (∀ i ∈ s, g i ≠ ⊤),
     by simpa [ennreal.rpow_eq_top_iff, asymm hpq.pos, asymm hpq.symm.pos, hpq.pos, hpq.symm.pos,
               ennreal.sum_eq_top_iff, not_or_distrib] using H',
@@ -447,7 +447,7 @@ theorem Lp_add_le (hp : 1 ≤ p) :
   (∑ i in s, (f i + g i) ^ p)^(1/p) ≤ (∑ i in s, (f i)^p) ^ (1/p) + (∑ i in s, (g i)^p) ^ (1/p) :=
 begin
   by_cases H' : (∑ i in s, (f i)^p) ^ (1/p) = ⊤ ∨ (∑ i in s, (g i)^p) ^ (1/p) = ⊤,
-  { cases H'; simp [H', -one_div_eq_inv] },
+  { cases H'; simp [H', -one_div] },
   have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
   replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ (∀ i ∈ s, g i ≠ ⊤),
     by simpa [ennreal.rpow_eq_top_iff, asymm pos, pos, ennreal.sum_eq_top_iff,
diff --git a/src/analysis/normed_space/banach.lean b/src/analysis/normed_space/banach.lean
@@ -131,7 +131,7 @@ begin
   have hnle : ∀n:ℕ, ∥(h^[n]) y∥ ≤ (1/2)^n * ∥y∥,
   { assume n,
     induction n with n IH,
-    { simp only [one_div_eq_inv, nat.nat_zero_eq_zero, one_mul, iterate_zero_apply,
+    { simp only [one_div, nat.nat_zero_eq_zero, one_mul, iterate_zero_apply,
         pow_zero] },
     { rw [iterate_succ'],
       apply le_trans (hle _) _,
diff --git a/src/analysis/special_functions/trigonometric.lean b/src/analysis/special_functions/trigonometric.lean
@@ -1259,7 +1259,7 @@ have h₂ : (x / sqrt (1 + x ^ 2)) ^ 2 < 1,
     exact mul_lt_one_of_nonneg_of_lt_one_left (abs_nonneg _)
       (abs_div_sqrt_one_add_lt _) (le_of_lt (abs_div_sqrt_one_add_lt _)),
 by rw [arctan, cos_arcsin (le_of_lt (neg_one_lt_div_sqrt_one_add _)) (le_of_lt (div_sqrt_one_add_lt_one _)),
-    one_div_eq_inv, ← sqrt_inv, sqrt_inj (sub_nonneg.2 (le_of_lt h₂)) (inv_nonneg.2 (le_of_lt h₁)),
+    one_div, ← sqrt_inv, sqrt_inj (sub_nonneg.2 (le_of_lt h₂)) (inv_nonneg.2 (le_of_lt h₁)),
     div_pow, pow_two (sqrt _), mul_self_sqrt (le_of_lt h₁),
     ← mul_right_inj' (ne.symm (ne_of_lt h₁)), mul_sub,
     mul_div_cancel' _ (ne.symm (ne_of_lt h₁)), mul_inv_cancel (ne.symm (ne_of_lt h₁))];
diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean
@@ -697,7 +697,7 @@ lemma self_div_two_le_harmonic_two_pow (n : ℕ) : (n / 2 : ℝ) ≤ harmonic_se
 begin
   induction n with n hn,
   unfold harmonic_series,
-  simp only [one_div_eq_inv, nat.cast_zero, euclidean_domain.zero_div, nat.cast_succ, sum_singleton,
+  simp only [one_div, nat.cast_zero, euclidean_domain.zero_div, nat.cast_succ, sum_singleton,
     inv_one, zero_add, nat.pow_zero, range_one, zero_le_one],
   have : harmonic_series (2^n) + 1 / 2 ≤ harmonic_series (2^(n+1)),
   { have := half_le_harmonic_double_sub_harmonic (2^n) (by {apply nat.pow_pos, linarith}),
diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean
@@ -258,7 +258,7 @@ theorem inv_def (z : ℂ) : z⁻¹ = conj z * ((norm_sq z)⁻¹:ℝ) := rfl
 ext_iff.2 $ begin
   simp,
   by_cases r = 0, { simp [h] },
-  { rw [← div_div_eq_div_mul, div_self h, one_div_eq_inv] },
+  { rw [← div_div_eq_div_mul, div_self h, one_div] },
 end
 
 protected lemma inv_zero : (0⁻¹ : ℂ) = 0 :=
diff --git a/src/data/complex/exponential.lean b/src/data/complex/exponential.lean
@@ -728,7 +728,7 @@ lemma sin_two_mul : sin (2 * x) = 2 * sin x * cos x :=
 by rw [two_mul, sin_add, two_mul, add_mul, mul_comm]
 
 lemma cos_square : cos x ^ 2 = 1 / 2 + cos (2 * x) / 2 :=
-by simp [cos_two_mul, div_add_div_same, mul_div_cancel_left, two_ne_zero', -one_div_eq_inv]
+by simp [cos_two_mul, div_add_div_same, mul_div_cancel_left, two_ne_zero', -one_div]
 
 lemma sin_square : sin x ^ 2 = 1 - cos x ^ 2 :=
 by { rw [←sin_sq_add_cos_sq x], simp }
@@ -964,7 +964,7 @@ calc ∑ m in filter (λ k, n ≤ k) (range j), (1 / m.fact : α)
 ... ≤ ∑ m in range (j - n), (nat.fact n * n.succ ^ m)⁻¹ :
   begin
     refine  sum_le_sum (assume m n, _),
-    rw [one_div_eq_inv, inv_le_inv],
+    rw [one_div, inv_le_inv],
     { rw [← nat.cast_pow, ← nat.cast_mul, nat.cast_le, add_comm],
       exact nat.fact_mul_pow_le_fact },
     { exact nat.cast_pos.2 (nat.fact_pos _) },
diff --git a/src/data/nat/cast.lean b/src/data/nat/cast.lean
@@ -160,7 +160,7 @@ lemma inv_pos_of_nat {n : ℕ} : 0 < ((n : α) + 1)⁻¹ :=
 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 }
+by { rw one_div, exact inv_pos_of_nat }
 
 lemma one_div_le_one_div {n m : ℕ} (h : n ≤ m) : 1 / ((m : α) + 1) ≤ 1 / ((n : α) + 1) :=
 by { refine one_div_le_one_div_of_le _ _, exact nat.cast_add_one_pos _, simpa }
diff --git a/src/data/real/conjugate_exponents.lean b/src/data/real/conjugate_exponents.lean
@@ -65,7 +65,7 @@ ne_of_gt (h.one_div_pos)
 lemma conj_eq : q = p/(p-1) :=
 begin
   have := h.inv_add_inv_conj,
-  rw [← eq_sub_iff_add_eq', one_div_eq_inv, inv_eq_iff] at this,
+  rw [← eq_sub_iff_add_eq', one_div, inv_eq_iff] at this,
   field_simp [← this, h.ne_zero]
 end
 
diff --git a/src/data/real/hyperreal.lean b/src/data/real/hyperreal.lean
@@ -689,7 +689,7 @@ lemma is_st_inv {x : ℝ*} {r : ℝ} (hi : ¬ infinitesimal x) : is_st x r → i
 have H : _ := exists_st_of_not_infinite $ not_imp_not.mpr (infinitesimal_iff_infinite_inv h).mpr hi,
 Exists.cases_on H $ λ s hs,
 have H' : is_st 1 (r * s) := mul_inv_cancel h ▸ is_st_mul hxr hs,
-have H'' : s = r⁻¹ := one_div_eq_inv r ▸ eq_one_div_of_mul_eq_one (eq_of_is_st_real H').symm,
+have H'' : s = r⁻¹ := one_div r ▸ eq_one_div_of_mul_eq_one (eq_of_is_st_real H').symm,
 H'' ▸ hs
 
 lemma st_inv (x : ℝ*) : st x⁻¹ = (st x)⁻¹ :=
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
@@ -594,7 +594,7 @@ by simpa using div_add_div b a one_ne_zero hc
   a / c + b = (a + b * c) / c :=
 by rwa [add_comm, add_div', add_comm]
 
-lemma one_div_eq_inv (a : ℝ≥0) : 1 / a = a⁻¹ :=
+lemma one_div (a : ℝ≥0) : 1 / a = a⁻¹ :=
 one_mul a⁻¹
 
 lemma one_div_div (a b : ℝ≥0) : 1 / (a / b) = b / a :=
diff --git a/src/measure_theory/simple_func_dense.lean b/src/measure_theory/simple_func_dense.lean
@@ -175,7 +175,7 @@ end,
 ( assume fx_eq_0 : f x = 0,
   have x_not_mem_A' : ∀ {M k}, x ∉ A' M k := λ M k,
   begin
-    simp only [mem_preimage, fx_eq_0, metric.mem_ball, one_div_eq_inv, norm_zero,
+    simp only [mem_preimage, fx_eq_0, metric.mem_ball, one_div, norm_zero,
                not_and, not_lt, add_comm, not_le, dist_zero_right, mem_diff],
     assume h, rw add_comm, exact inv_pos_of_nat
   end,
@@ -193,7 +193,7 @@ end,
     let ⟨k, hk⟩ := mem_closure_range_iff_nat.1 (by { rw E_dense, exact mem_univ (f x) }) N₀ in
     begin
       rw [Union_disjointed, mem_Union], use k,
-      rw [mem_preimage], simp, rw [← one_div_eq_inv],
+      rw [mem_preimage], simp, rw [← one_div],
       exact ⟨hk, le_of_lt norm_fx_gt⟩
     end,
   let ⟨k₀, x_mem_A⟩ := mem_Union.1 x_mem_Union_k_N₀ in
diff --git a/src/tactic/interactive.lean b/src/tactic/interactive.lean
@@ -729,7 +729,7 @@ iterating the following steps:
 If the goal is an equality, this simpset will also clear the denominators, so that the proof
 can normally be concluded by an application of `ring` or `ring_exp`.
 
-`field_simp [hx, hy]` is a short form for `simp [-one_div_eq_inv, hx, hy] with field_simps`
+`field_simp [hx, hy]` is a short form for `simp [-one_div, hx, hy] with field_simps`
 
 Note that this naive algorithm will not try to detect common factors in denominators to reduce the
 complexity of the resulting expression. Instead, it relies on the ability of `ring` to handle
@@ -743,7 +743,7 @@ should be given explicitly. If your expression is not completely reduced by the
 invocation, check the denominators of the resulting expression and provide proofs that they are
 nonzero to enable further progress.
 
-The invocation of `field_simp` removes the lemma `one_div_eq_inv` (which is marked as a simp lemma
+The invocation of `field_simp` removes the lemma `one_div` (which is marked as a simp lemma
 in core) from the simpset, as this lemma works against the algorithm explained above.
 
 For example,
@@ -765,7 +765,7 @@ meta def field_simp (no_dflt : parse only_flag) (hs : parse simp_arg_list)
   (attr_names : parse with_ident_list)
   (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
 let attr_names := `field_simps :: attr_names,
-    hs := simp_arg_type.except `one_div_eq_inv :: hs in
+    hs := simp_arg_type.except `one_div :: hs in
 propagate_tags (simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat)
 
 add_tactic_doc
diff --git a/src/tactic/norm_num.lean b/src/tactic/norm_num.lean
@@ -434,7 +434,7 @@ h ▸ by simp only [inv_eq_one_div, one_div_neg_eq_neg_one_div]
 
 theorem inv_one {α} [division_ring α] : (1 : α)⁻¹ = 1 := inv_one
 theorem inv_one_div {α} [division_ring α] (a : α) : (1 / a)⁻¹ = a :=
-by rw [one_div_eq_inv, inv_inv']
+by rw [one_div, inv_inv']
 theorem inv_div_one {α} [division_ring α] (a : α) : a⁻¹ = 1 / a :=
 inv_eq_one_div _
 theorem inv_div {α} [division_ring α] (a b : α) : (a / b)⁻¹ = b / a :=
diff --git a/src/topology/metric_space/pi_Lp.lean b/src/topology/metric_space/pi_Lp.lean
@@ -132,7 +132,7 @@ begin
   assume i,
   calc
   edist (x i) (y i) = (edist (x i) (y i) ^ p) ^ (1/p) :
-    by simp [← ennreal.rpow_mul, cancel, -one_div_eq_inv]
+    by simp [← ennreal.rpow_mul, cancel, -one_div]
   ... ≤ (∑ (i : ι), edist (x i) (y i) ^ p) ^ (1 / p) :
   begin
     apply ennreal.rpow_le_rpow _ (one_div_nonneg.2 $ le_of_lt pos),
@@ -147,7 +147,7 @@ begin
   have nonneg : 0 ≤ 1 / p := one_div_nonneg.2 (le_of_lt pos),
   have cancel : p * (1/p) = 1 := mul_div_cancel' 1 (ne_of_gt pos),
   assume x y,
-  simp [edist, -one_div_eq_inv],
+  simp [edist, -one_div],
   calc (∑ (i : ι), edist (x i) (y i) ^ p) ^ (1 / p) ≤
   (∑ (i : ι), edist (pi_Lp.equiv p hp α x) (pi_Lp.equiv p hp α y) ^ p) ^ (1 / p) :
   begin
@@ -211,7 +211,7 @@ begin
           ennreal.sum_eq_top_iff, edist_ne_top] },
   { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p < ⊤ :=
       λ i hi, by simp [lt_top_iff_ne_top, edist_ne_top, le_of_lt pos],
-    simp [dist, -one_div_eq_inv, pi_Lp.edist, ← ennreal.to_real_rpow,
+    simp [dist, -one_div, pi_Lp.edist, ← ennreal.to_real_rpow,
           ennreal.to_real_sum A, dist_edist] }
 end
 
