chore(tactic/monotonicity/lemmas): Move lemmas to the correct places (#…

…16509)

A few lemmas were gathered in `tactic.monotonicity.lemmas` rather than the files they belong to. Generalize them, move them and fix their names.

src/algebra/order/ring.lean

@@ -1164,6 +1164,12 @@ lemma neg_one_lt_zero : -1 < (0:α) := neg_lt_zero.2 zero_lt_one
 @[simp] lemma mul_lt_mul_right_of_neg {a b c : α} (h : c < 0) : a * c < b * c ↔ b < a :=
 (strict_anti_mul_right h).lt_iff_lt
 
+lemma lt_of_mul_lt_mul_of_nonpos_left (h : c * a < c * b) (hc : c ≤ 0) : b < a :=
+lt_of_mul_lt_mul_left (by rwa [neg_mul, neg_mul, neg_lt_neg_iff]) $ neg_nonneg.2 hc
+
+lemma lt_of_mul_lt_mul_of_nonpos_right (h : a * c < b * c) (hc : c ≤ 0) : b < a :=
+lt_of_mul_lt_mul_right (by rwa [mul_neg, mul_neg, neg_lt_neg_iff]) $ neg_nonneg.2 hc
+
 lemma cmp_mul_neg_left {a : α} (ha : a < 0) (b c : α) : cmp (a * b) (a * c) = cmp c b :=
 (strict_anti_mul_left ha).cmp_map_eq b c
 

src/algebra/order/sub.lean

@@ -500,29 +500,29 @@ protected lemma lt_tsub_iff_left_of_le (hc : add_le_cancellable c) (h : c ≤ b)
   a < b - c ↔ c + a < b :=
 by { rw [add_comm], exact hc.lt_tsub_iff_right_of_le h }
 
+protected lemma tsub_inj_right (hab : add_le_cancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a)
+  (h₃ : a - b = a - c) : b = c :=
+by { rw ← hab.inj, rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂] }
+
 protected lemma lt_of_tsub_lt_tsub_left_of_le [contravariant_class α α (+) (<)]
   (hb : add_le_cancellable b) (hca : c ≤ a) (h : a - b < a - c) : c < b :=
 begin
   conv_lhs at h { rw [← tsub_add_cancel_of_le hca] },
   exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h),
 end
 
+protected lemma tsub_lt_tsub_left_of_le (hab : add_le_cancellable (a - b)) (h₁ : b ≤ a)
+  (h : c < b) : a - b < a - c :=
+(tsub_le_tsub_left h.le _).lt_of_ne $ λ h', h.ne' $ hab.tsub_inj_right h₁ (h.le.trans h₁) h'
+
 protected lemma tsub_lt_tsub_right_of_le (hc : add_le_cancellable c) (h : c ≤ a) (h2 : a < b) :
   a - c < b - c :=
 by { apply hc.lt_tsub_of_add_lt_left, rwa [add_tsub_cancel_of_le h] }
 
-protected lemma tsub_inj_right (hab : add_le_cancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a)
-  (h₃ : a - b = a - c) : b = c :=
-by { rw ← hab.inj, rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂] }
-
 protected lemma tsub_lt_tsub_iff_left_of_le_of_le [contravariant_class α α (+) (<)]
   (hb : add_le_cancellable b) (hab : add_le_cancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) :
   a - b < a - c ↔ c < b :=
-begin
-  refine ⟨hb.lt_of_tsub_lt_tsub_left_of_le h₂, _⟩,
-  intro h, refine (tsub_le_tsub_left h.le _).lt_of_ne _,
-  rintro h2, exact h.ne' (hab.tsub_inj_right h₁ h₂ h2)
-end
+⟨hb.lt_of_tsub_lt_tsub_left_of_le h₂, hab.tsub_lt_tsub_left_of_le h₁⟩
 
 @[simp] protected lemma add_tsub_tsub_cancel (hac : add_le_cancellable (a - c)) (h : c ≤ a) :
   (a + b) - (a - c) = b + c :=
@@ -588,6 +588,9 @@ lemma lt_of_tsub_lt_tsub_left_of_le  [contravariant_class α α (+) (<)]
   (hca : c ≤ a) (h : a - b < a - c) : c < b :=
 contravariant.add_le_cancellable.lt_of_tsub_lt_tsub_left_of_le hca h
 
+lemma tsub_lt_tsub_left_of_le : b ≤ a → c < b → a - b < a - c :=
+contravariant.add_le_cancellable.tsub_lt_tsub_left_of_le
+
 lemma tsub_lt_tsub_right_of_le (h : c ≤ a) (h2 : a < b) : a - c < b - c :=
 contravariant.add_le_cancellable.tsub_lt_tsub_right_of_le h h2
 

src/analysis/calculus/taylor.lean

@@ -356,16 +356,15 @@ begin
   have h' : ∀ (y : ℝ) (hy : y ∈ Ico a x),
     ∥((n! : ℝ)⁻¹ * (x - y) ^ n) • iterated_deriv_within (n + 1) f (Icc a b) y∥
     ≤ (n! : ℝ)⁻¹ * |(x - a)|^n * C,
-  { intros y hy,
+  { rintro y ⟨hay, hyx⟩,
     rw [norm_smul, real.norm_eq_abs],
     -- Estimate the iterated derivative by `C`
-    refine mul_le_mul _ (hC y ⟨hy.1, hy.2.le.trans hx.2⟩) (by positivity) (by positivity),
+    refine mul_le_mul _ (hC y ⟨hay, hyx.le.trans hx.2⟩) (by positivity) (by positivity),
     -- The rest is a trivial calculation
     rw [abs_mul, abs_pow, abs_inv, nat.abs_cast],
-    mono*,
+    mono* with [0 ≤ (n! : ℝ)⁻¹],
     any_goals { positivity },
-    { exact hy.1 },
-    { linarith [hx.1, hy.2] } },
+    linarith [hx.1, hyx] },
   -- Apply the mean value theorem for vector valued functions:
   have A : ∀ t ∈ Icc a x, has_deriv_within_at (λ y, taylor_within_eval f n (Icc a b) y x)
     (((↑n!)⁻¹ * (x - t) ^ n) • iterated_deriv_within (n + 1) f (Icc a b) t) (Icc a x) t,

src/analysis/inner_product_space/projection.lean

@@ -123,7 +123,8 @@ begin
         repeat {exact le_of_lt one_half_pos},
         exact add_halves 1 },
     have eq₁ : 4 * δ * δ ≤ 4 * ∥u - half • (wq + wp)∥ * ∥u - half • (wq + wp)∥,
-    { mono, mono, norm_num, apply mul_nonneg, norm_num, exact norm_nonneg _ },
+    { simp_rw mul_assoc,
+      exact mul_le_mul_of_nonneg_left (mul_self_le_mul_self zero_le_δ eq) zero_le_four },
     have eq₂ : ∥a∥ * ∥a∥ ≤ (δ + div) * (δ + div) :=
       mul_self_le_mul_self (norm_nonneg _)
         (le_trans (le_of_lt $ hw q) (add_le_add_left (nat.one_div_le_one_div hq) _)),

src/data/bitvec/basic.lean

@@ -46,8 +46,8 @@ begin
     rw [add_lsb_eq_twice_add_one],
     transitivity 2 * list.foldr (λ (x : bool) (y : ℕ), add_lsb y x) 0 ys_tl + 2 * 1,
     { ac_mono, rw two_mul, mono, cases ys_hd; simp },
-    { rw ← left_distrib, ac_mono, norm_num,
-      apply ys_ih, refl } },
+    { rw ← left_distrib, ac_mono,
+      exact ys_ih rfl, norm_num } }
 end
 
 lemma add_lsb_div_two {x b} : add_lsb x b / 2 = x :=

src/number_theory/liouville/liouville_constant.lean

@@ -123,8 +123,7 @@ lemma aux_calc (n : ℕ) {m : ℝ} (hm : 2 ≤ m) :
 calc (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!) :
   -- the second factors coincide (and are non-negative),
   -- the first factors, satisfy the inequality `sub_one_div_inv_le_two`
-  mul_mono_nonneg (one_div_nonneg.mpr (pow_nonneg (zero_le_two.trans hm) _))
-    (sub_one_div_inv_le_two hm)
+  mul_le_mul_of_nonneg_right (sub_one_div_inv_le_two hm) (by positivity)
 ... = 2 / m ^ (n + 1)! : mul_one_div 2 _
 ... = 2 / m ^ (n! * (n + 1)) : congr_arg ((/) 2) (congr_arg (pow m) (mul_comm _ _))
 ... ≤ 1 / m ^ (n! * n) :

src/tactic/monotonicity/lemmas.lean

@@ -4,70 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
 import algebra.order.ring
-import data.nat.basic
 import data.set.lattice
-import order.directed
 import tactic.monotonicity.basic
 
 variables {α : Type*}
 
-@[mono]
-lemma mul_mono_nonneg {x y z : α} [ordered_semiring α]
-  (h' : 0 ≤ z)
-  (h : x ≤ y)
-: x * z ≤ y * z :=
-by apply mul_le_mul_of_nonneg_right; assumption
-
-lemma lt_of_mul_lt_mul_neg_right {a b c : α}  [linear_ordered_ring α]
-  (h : a * c < b * c) (hc : c ≤ 0) : b < a :=
-have nhc : -c ≥ 0, from neg_nonneg_of_nonpos hc,
-have h2 : -(b * c) < -(a * c), from neg_lt_neg h,
-have h3 : b * (-c) < a * (-c), from calc
-     b * (-c) = - (b * c)    : by rewrite neg_mul_eq_mul_neg
-          ... < - (a * c)    : h2
-          ... = a * (-c)     : by rewrite neg_mul_eq_mul_neg,
-lt_of_mul_lt_mul_right h3 nhc
-
-@[mono]
-lemma mul_mono_nonpos {x y z : α} [linear_ordered_ring α]
-  (h' : z ≤ 0) (h : y ≤ x) : x * z ≤ y * z :=
-begin
-  classical,
-  by_contradiction h'',
-  revert h,
-  apply not_le_of_lt,
-  apply lt_of_mul_lt_mul_neg_right _ h',
-  apply lt_of_not_ge h''
-end
-
-@[mono]
-lemma nat.sub_mono_left_strict {x y z : ℕ}
-  (h' : z ≤ x)
-  (h : x < y)
-: x - z < y - z :=
-begin
-  have : z ≤ y,
-  { transitivity, assumption, apply le_of_lt h, },
-  apply @nat.lt_of_add_lt_add_left z,
-  rw [add_tsub_cancel_of_le,add_tsub_cancel_of_le];
-    solve_by_elim
-end
-
-@[mono]
-lemma nat.sub_mono_right_strict {x y z : ℕ}
-  (h' : x ≤ z)
-  (h : y < x)
-: z - x < z - y :=
-begin
-  have h'' : y ≤ z,
-  { transitivity, apply le_of_lt h, assumption },
-  apply @nat.lt_of_add_lt_add_right _ x,
-  rw [tsub_add_cancel_of_le h'],
-  apply @lt_of_le_of_lt _ _ _ (z - y + y),
-  rw [tsub_add_cancel_of_le h''],
-  apply nat.add_lt_add_left h
-end
-
 open set
 
 attribute [mono] inter_subset_inter union_subset_union
@@ -81,7 +22,10 @@ attribute [mono] upper_bounds_mono_set lower_bounds_mono_set
 
 attribute [mono] add_le_add mul_le_mul neg_le_neg
          mul_lt_mul_of_pos_left mul_lt_mul_of_pos_right
+         mul_le_mul_of_nonneg_left mul_le_mul_of_nonneg_right
+         mul_le_mul_of_nonpos_left mul_le_mul_of_nonpos_right
          imp_imp_imp le_implies_le_of_le_of_le
+         tsub_lt_tsub_left_of_le tsub_lt_tsub_right_of_le
          tsub_le_tsub abs_le_abs sup_le_sup
          inf_le_inf
 attribute [mono left] add_lt_add_of_le_of_lt mul_lt_mul'