refactor(data/real/ennreal): remove ordered sub simp lemmas (#9902)

* They are now simp lemmas in `algebra/order/sub`
* Squeeze some simps

src/algebra/order/sub.lean

@@ -327,7 +327,7 @@ end linear_order
 section canonically_ordered_add_monoid
 variables [canonically_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c d : α}
 
-lemma add_tsub_cancel_of_le (h : a ≤ b) : a + (b - a) = b :=
+@[simp] lemma add_tsub_cancel_of_le (h : a ≤ b) : a + (b - a) = b :=
 begin
   refine le_antisymm _ le_add_tsub,
   obtain ⟨c, rfl⟩ := le_iff_exists_add.1 h,
@@ -359,9 +359,13 @@ by simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h
 lemma lt_of_tsub_lt_tsub_right_of_le (h : c ≤ b) (h2 : a - c < b - c) : a < b :=
 by { refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne _, rintro rfl, exact h2.false }
 
-lemma tsub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b :=
+@[simp] lemma tsub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b :=
 by rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
 
+/-- One direction of `tsub_eq_zero_iff_le`, as a `@[simp]`-lemma. -/
+@[simp] lemma tsub_eq_zero_of_le (h : a ≤ b) : a - b = 0 :=
+tsub_eq_zero_iff_le.mpr h
+
 @[simp] lemma tsub_self (a : α) : a - a = 0 :=
 tsub_eq_zero_iff_le.mpr le_rfl
 
@@ -620,7 +624,7 @@ end canonically_ordered_add_monoid
 section canonically_linear_ordered_add_monoid
 variables [canonically_linear_ordered_add_monoid α] [has_sub α] [has_ordered_sub α] {a b c d : α}
 
-lemma tsub_pos_iff_lt : 0 < a - b ↔ b < a :=
+@[simp] lemma tsub_pos_iff_lt : 0 < a - b ↔ b < a :=
 by rw [tsub_pos_iff_not_le, not_le]
 
 lemma tsub_eq_tsub_min (a b : α) : a - b = a - min a b :=

src/analysis/special_functions/integrals.lean

@@ -314,7 +314,7 @@ begin
   let C := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b,
   have h : ∀ α β γ : ℝ, α * (β * α * γ) = β * (α * α * γ) := λ α β γ, by ring,
   have hu : ∀ x ∈ _, has_deriv_at (λ y, sin y ^ (n + 1)) ((n + 1) * cos x * sin x ^ n) x :=
-    λ x hx, by simpa [mul_right_comm] using (has_deriv_at_sin x).pow,
+    λ x hx, by simpa only [mul_right_comm] using (has_deriv_at_sin x).pow,
   have hv : ∀ x ∈ [a, b], has_deriv_at (-cos) (sin x) x :=
     λ x hx, by simpa only [neg_neg] using (has_deriv_at_cos x).neg,
   have H := integral_mul_deriv_eq_deriv_mul hu hv _ _,
@@ -386,7 +386,8 @@ begin
   let C := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a,
   have h : ∀ α β γ : ℝ, α * (β * α * γ) = β * (α * α * γ) := λ α β γ, by ring,
   have hu : ∀ x ∈ _, has_deriv_at (λ y, cos y ^ (n + 1)) (-(n + 1) * sin x * cos x ^ n) x :=
-    λ x hx, by simpa [mul_right_comm, -neg_add_rev] using (has_deriv_at_cos x).pow,
+    λ x hx, by simpa only [mul_right_comm, neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm]
+      using (has_deriv_at_cos x).pow,
   have hv : ∀ x ∈ [a, b], has_deriv_at sin (cos x) x := λ x hx, has_deriv_at_sin x,
   have H := integral_mul_deriv_eq_deriv_mul hu hv _ _,
   calc  ∫ x in a..b, cos x ^ (n + 2)

src/analysis/specific_limits.lean

@@ -401,7 +401,7 @@ begin
     norm_cast at *,
     convert ennreal.tsum_coe_eq (nnreal.has_sum_geometric hr),
     rw [ennreal.coe_inv $ ne_of_gt $ tsub_pos_iff_lt.2 hr] },
-  { rw [ennreal.sub_eq_zero_of_le hr, ennreal.inv_zero, ennreal.tsum_eq_supr_nat, supr_eq_top],
+  { rw [tsub_eq_zero_iff_le.mpr hr, ennreal.inv_zero, ennreal.tsum_eq_supr_nat, supr_eq_top],
     refine λ a ha, (ennreal.exists_nat_gt (lt_top_iff_ne_top.1 ha)).imp
       (λ n hn, lt_of_lt_of_le hn _),
     calc (n:ℝ≥0∞) = ∑ i in range n, 1     : by rw [sum_const, nsmul_one, card_range]
@@ -515,7 +515,7 @@ begin
   refine cauchy_seq_of_edist_le_of_tsum_ne_top _ hu _,
   rw [ennreal.tsum_mul_left, ennreal.tsum_geometric],
   refine ennreal.mul_ne_top hC (ennreal.inv_ne_top.2 _),
-  exact (ennreal.sub_pos.2 hr).ne'
+  exact (tsub_pos_iff_lt.2 hr).ne'
 end
 
 omit hr hC

src/computability/halting.lean

@@ -315,13 +315,14 @@ theorem rfind_opt {n} {f : vector ℕ (n+1) → ℕ}
    .comp₁ (λ n, part.some (1 - n)) hf)
    .bind ((prim nat.primrec'.pred).comp₁ nat.pred hf)).of_eq $
 λ v, part.ext $ λ b, begin
-  simp [nat.rfind_opt, -nat.mem_rfind],
+  simp only [nat.rfind_opt, exists_prop, tsub_eq_zero_iff_le, pfun.coe_val,
+    part.mem_bind_iff, part.mem_some_iff, option.mem_def, part.mem_coe],
   refine exists_congr (λ a,
     (and_congr (iff_of_eq _) iff.rfl).trans (and_congr_right (λ h, _))),
-  { congr; funext n,
-    simp, cases f (n ::ᵥ v); simp [nat.succ_ne_zero]; refl },
+  { congr, funext n,
+    simp only [part.some_inj, pfun.coe_val], cases f (n ::ᵥ v); simp [nat.succ_le_succ]; refl },
   { have := nat.rfind_spec h,
-    simp at this,
+    simp only [pfun.coe_val, part.mem_some_iff] at this,
     cases f (a ::ᵥ v) with c, {cases this},
     rw [← option.some_inj, eq_comm], refl }
 end

src/data/real/ennreal.lean

@@ -730,22 +730,6 @@ by simp
 lemma sub_top : a - ∞ = 0 :=
 by simp
 
--- todo: make this a `@[simp]` lemma in general
-@[simp] lemma sub_eq_zero_of_le (h : a ≤ b) : a - b = 0 :=
-tsub_eq_zero_iff_le.mpr h
-
--- todo: make `add_tsub_cancel_of_le` a `@[simp]` lemma
-@[simp] protected lemma add_sub_cancel_of_le (h : b ≤ a) : b + (a - b) = a :=
-add_tsub_cancel_of_le h
-
--- todo: make `tsub_eq_zero_iff_le` a `@[simp]` lemma
-@[simp] protected lemma sub_eq_zero_iff_le : a - b = 0 ↔ a ≤ b :=
-tsub_eq_zero_iff_le
-
--- todo: make `tsub_pos_iff_lt` a `@[simp]` lemma
-@[simp] protected lemma sub_pos : 0 < a - b ↔ b < a :=
-tsub_pos_iff_lt
-
 lemma sub_eq_top_iff : a - b = ∞ ↔ a = ∞ ∧ b ≠ ∞ :=
 by { cases a; cases b; simp [← with_top.coe_sub] }
 

src/measure_theory/decomposition/lebesgue.lean

@@ -655,7 +655,7 @@ theorem have_lebesgue_decomposition_of_finite_measure [is_finite_measure μ] [is
   -- since `ν.with_density ξ ≤ μ`, it is clear that `μ = μ₁ + ν.with_density ξ`
   { rw hμ₁, ext1 A hA,
     rw [measure.coe_add, pi.add_apply, measure.sub_apply hA hle,
-        add_comm, ennreal.add_sub_cancel_of_le (hle A hA)] },
+        add_comm, add_tsub_cancel_of_le (hle A hA)] },
 end⟩
 
 local attribute [instance] have_lebesgue_decomposition_of_finite_measure

src/measure_theory/integral/lebesgue.lean

@@ -607,7 +607,7 @@ begin
   { simp only [nat.nat_zero_eq_zero, finset.sum_singleton, finset.range_one], refl },
   { rw [finset.sum_range_succ, nat.succ_eq_add_one, IH, eapprox_diff, coe_map, function.comp_app,
         coe_sub, pi.sub_apply, ennreal.coe_to_nnreal,
-        ennreal.add_sub_cancel_of_le (monotone_eapprox f (nat.le_succ _) _)],
+        add_tsub_cancel_of_le (monotone_eapprox f (nat.le_succ _) _)],
     apply (lt_of_le_of_lt _ (eapprox_lt_top f (n+1) a)).ne,
     rw tsub_le_iff_right,
     exact le_self_add },
@@ -1266,7 +1266,7 @@ begin
   rcases exists_between hε₂0 with ⟨ε₁, hε₁0, hε₁₂⟩,
   rcases exists_simple_func_forall_lintegral_sub_lt_of_pos h hε₁0.ne' with ⟨φ, hle, hφ⟩,
   rcases φ.exists_forall_le with ⟨C, hC⟩,
-  use [(ε₂ - ε₁) / C, ennreal.div_pos_iff.2 ⟨(ennreal.sub_pos.2 hε₁₂).ne', ennreal.coe_ne_top⟩],
+  use [(ε₂ - ε₁) / C, ennreal.div_pos_iff.2 ⟨(tsub_pos_iff_lt.2 hε₁₂).ne', ennreal.coe_ne_top⟩],
   refine λ s hs, lt_of_le_of_lt _ hε₂ε,
   simp only [lintegral_eq_nnreal, supr_le_iff],
   intros ψ hψ,
@@ -1612,10 +1612,10 @@ lemma lintegral_strict_mono_of_ae_le_of_ae_lt_on {f g : α → ℝ≥0∞}
   {s : set α} (hμs : μ s ≠ 0) (h : ∀ᵐ x ∂μ, x ∈ s → f x < g x) :
   ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ :=
 begin
-  rw [← ennreal.sub_pos, ← lintegral_sub hg hf hfi h_le],
+  rw [← tsub_pos_iff_lt, ← lintegral_sub hg hf hfi h_le],
   by_contra hnlt,
   rw [not_lt, nonpos_iff_eq_zero, lintegral_eq_zero_iff (hg.sub hf), filter.eventually_eq] at hnlt,
-  simp only [ae_iff, ennreal.sub_eq_zero_iff_le, pi.zero_apply, not_lt, not_le] at hnlt h,
+  simp only [ae_iff, tsub_eq_zero_iff_le, pi.zero_apply, not_lt, not_le] at hnlt h,
   refine hμs _,
   push_neg at h,
   have hs_eq : s = {a : α | a ∈ s ∧ g a ≤ f a} ∪ {a : α | a ∈ s ∧ f a < g a},

src/measure_theory/measure/regular.lean

@@ -307,7 +307,7 @@ begin
       λ n, (inter_subset_right _ _).trans (disjointed_subset _ _),
       (disjoint_disjointed s.set).mono (λ k l hkl, hkl.mono inf_le_right inf_le_right), _⟩,
     rw [← inter_Union, Union_disjointed, s.spanning, inter_univ] },
-  rcases ennreal.exists_pos_sum_of_encodable' (ennreal.sub_pos.2 hr).ne' ℕ with ⟨δ, δ0, hδε⟩,
+  rcases ennreal.exists_pos_sum_of_encodable' (tsub_pos_iff_lt.2 hr).ne' ℕ with ⟨δ, δ0, hδε⟩,
   rw [lt_tsub_iff_right, add_comm] at hδε,
   have : ∀ n, ∃ U ⊇ A n, is_open U ∧ μ U < μ (A n) + δ n,
   { intro n,
@@ -364,9 +364,9 @@ begin
     ∃ (F ⊆ s) (U ⊇ s), is_closed F ∧ is_open U ∧ μ s ≤ μ F + ε ∧ μ U ≤ μ s + ε,
   { refine { outer_regular := λ s hs r hr, _, inner_regular := H },
     rcases exists_between hr with ⟨r', hsr', hr'r⟩,
-    rcases this s hs _ (ennreal.sub_pos.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩,
+    rcases this s hs _ (tsub_pos_iff_lt.2 hsr').ne' with ⟨-, -, U, hsU, -, hUo, -, H⟩,
     refine ⟨U, hsU, hUo, _⟩,
-    rw [ennreal.add_sub_cancel_of_le hsr'.le] at H, exact H.trans_lt hr'r },
+    rw [add_tsub_cancel_of_le hsr'.le] at H, exact H.trans_lt hr'r },
   refine measurable_set.induction_on_open _ _ _,
   /- The proof is by measurable induction: we should check that the property is true for the empty
   set, for open sets, and is stable by taking the complement and by taking countable disjoint

src/topology/instances/ennreal.lean

@@ -215,13 +215,13 @@ begin
   rw nhds_generate_from, refine le_infi (assume s, le_infi $ assume hs, _),
   rcases hs with ⟨xs, ⟨a, (rfl : s = Ioi a)|(rfl : s = Iio a)⟩⟩,
   { rcases exists_between xs with ⟨b, ab, bx⟩,
-    have xb_pos : 0 < x - b := ennreal.sub_pos.2 bx,
+    have xb_pos : 0 < x - b := tsub_pos_iff_lt.2 bx,
     have xxb : x - (x - b) = b := sub_sub_cancel xt bx.le,
     refine infi_le_of_le (x - b) (infi_le_of_le xb_pos _),
     simp only [mem_principal, le_principal_iff],
     assume y, rintros ⟨h₁, h₂⟩, rw xxb at h₁, calc a < b : ab ... ≤ y : h₁ },
   { rcases exists_between xs with ⟨b, xb, ba⟩,
-    have bx_pos : 0 < b - x := ennreal.sub_pos.2 xb,
+    have bx_pos : 0 < b - x := tsub_pos_iff_lt.2 xb,
     have xbx : x + (b - x) = b := add_tsub_cancel_of_le xb.le,
     refine infi_le_of_le (b - x) (infi_le_of_le bx_pos _),
     simp only [mem_principal, le_principal_iff],

src/topology/metric_space/emetric_space.lean

@@ -523,8 +523,7 @@ theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε'
 begin
   have : 0 < ε - edist y x := by simpa using h,
   refine ⟨ε - edist y x, this, ball_subset _ (ne_top_of_lt h)⟩,
-  rw ennreal.add_sub_cancel_of_le (le_of_lt h),
-  exact le_refl ε
+  exact (add_tsub_cancel_of_le (mem_ball.mp h).le).le
 end
 
 theorem ball_eq_empty_iff : ball x ε = ∅ ↔ ε = 0 :=