diff --git a/src/algebra/order/sub.lean b/src/algebra/order/sub.lean index e5a4773e8c3a6..f8cf147fdaad4 100644 --- a/src/algebra/order/sub.lean +++ b/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 := diff --git a/src/analysis/special_functions/integrals.lean b/src/analysis/special_functions/integrals.lean index 5c9265092f5d4..948ee9f89c7a7 100644 --- a/src/analysis/special_functions/integrals.lean +++ 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) diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean index 6a0d97182e2bb..de5334013b83f 100644 --- a/src/analysis/specific_limits.lean +++ b/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 diff --git a/src/computability/halting.lean b/src/computability/halting.lean index 96b598de66299..8264fea17b01f 100644 --- a/src/computability/halting.lean +++ b/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 diff --git a/src/data/real/ennreal.lean b/src/data/real/ennreal.lean index fa6bcdb17d76c..d27b38b951e22 100644 --- a/src/data/real/ennreal.lean +++ b/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] } diff --git a/src/measure_theory/decomposition/lebesgue.lean b/src/measure_theory/decomposition/lebesgue.lean index 5f0d7e9019184..3e6172d389969 100644 --- a/src/measure_theory/decomposition/lebesgue.lean +++ b/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 diff --git a/src/measure_theory/integral/lebesgue.lean b/src/measure_theory/integral/lebesgue.lean index 42a32ce9fbf5c..ecef358eaa22f 100644 --- a/src/measure_theory/integral/lebesgue.lean +++ b/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}, diff --git a/src/measure_theory/measure/regular.lean b/src/measure_theory/measure/regular.lean index 4216ef579a310..60c7cb66ffc34 100644 --- a/src/measure_theory/measure/regular.lean +++ b/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 diff --git a/src/topology/instances/ennreal.lean b/src/topology/instances/ennreal.lean index 53ec4a1cefc1f..21adceeb3b743 100644 --- a/src/topology/instances/ennreal.lean +++ b/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], diff --git a/src/topology/metric_space/emetric_space.lean b/src/topology/metric_space/emetric_space.lean index d2a2769bde22d..202540918cb66 100644 --- a/src/topology/metric_space/emetric_space.lean +++ b/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 :=