chore(*): golf using new positivity tactic (#15701)

The `positivity` tactic introduced in #15618 solves goals of the form `0 < x` and `0 ≤ x`, particularly motivated by streamlining bigger inequality calculations where these frequently show up as side goals.  This PR gives a few example uses in this kind of bigger inequality calculation, golfing proofs in: 
- archive/imo/imo2005_q3
- archive/imo/imo2013_q5
- analysis/convex/basic
- analysis/mean_inequalities_pow
- topology/algebra/order/basic

archive/imo/imo2005_q3.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Manuel Candales
 -/
 import data.real.basic
+import tactic.positivity
 
 /-!
 # IMO 2005 Q3
@@ -20,21 +21,17 @@ and then making use of `xyz ≥ 1` to show `(x^5-x^2)/(x^3*(x^2+y^2+z^2)) ≥ (x
 lemma key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) :
   (x^5-x^2)/(x^5+y^2+z^2) ≥ (x^2-y*z)/(x^2+y^2+z^2) :=
 begin
-  have h₁ : 0 < x^5+y^2+z^2, linarith [pow_pos hx 5, pow_pos hy 2, pow_pos hz 2],
-  have h₂ : 0 < x^3, exact pow_pos hx 3,
-  have h₃ : 0 < x^2+y^2+z^2, linarith [pow_pos hx 2, pow_pos hy 2, pow_pos hz 2],
-  have h₄ : 0 < x^3*(x^2+y^2+z^2), exact mul_pos h₂ h₃,
+  have h₁ : 0 < x^5+y^2+z^2 := by positivity,
+  have h₂ : 0 < x^3 := by positivity,
+  have h₃ : 0 < x^2+y^2+z^2 := by positivity,
+  have h₄ : 0 < x^3*(x^2+y^2+z^2) := by positivity,
 
   have key : (x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2))
            = ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))),
   { field_simp [h₁.ne', h₄.ne'],
     ring },
 
-  have h₅ : ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))) ≥ 0,
-  { refine div_nonneg _ _,
-    refine mul_nonneg (mul_nonneg (sq_nonneg _) (sq_nonneg _)) _,
-    exact add_nonneg (sq_nonneg _) (sq_nonneg _),
-    exact le_of_lt (mul_pos h₁ h₄) },
+  have h₅ : ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))) ≥ 0 := by positivity,
 
   calc  (x^5-x^2)/(x^5+y^2+z^2)
       ≥ (x^5-x^2)/(x^3*(x^2+y^2+z^2)) : by linarith [key, h₅]

archive/imo/imo2013_q5.lean

@@ -7,6 +7,7 @@ Authors: David Renshaw
 import algebra.geom_sum
 import data.rat.defs
 import data.real.basic
+import tactic.positivity
 
 /-!
 # IMO 2013 Q5
@@ -142,7 +143,7 @@ begin
   { simp only [pow_one] },
   have hpn' := hpn pn.succ_pos,
   rw [pow_succ' x (pn + 1), pow_succ' (f x) (pn + 1)],
-  have hxp : 0 < x := zero_lt_one.trans hx,
+  have hxp : 0 < x := by positivity,
   calc f ((x ^ (pn+1)) * x)
           ≤ f (x ^ (pn+1)) * f x : H1 (x ^ (pn+1)) x (pow_pos hxp (pn+1)) hxp
       ... ≤ (f x) ^ (pn+1) * f x : (mul_le_mul_right (f_pos_of_pos hxp H1 H4)).mpr hpn'
@@ -180,7 +181,7 @@ begin
                         ≤ f x + ((a^N - x) : ℚ) : add_le_add_right (H5 x hx) _
                     ... ≤ f x + f (a^N - x)     : add_le_add_left (H5 _ h_big_enough) _,
 
-  have hxp : 0 < x := zero_lt_one.trans hx,
+  have hxp : 0 < x := by positivity,
 
   have hNp : 0 < N,
   { by_contra' H, rw [nat.le_zero_iff.mp H] at hN, linarith },
@@ -244,7 +245,7 @@ begin
                                           H1 H2 H4
                      ... ≤ (f x)^n : pow_f_le_f_pow hn hx H1 H4 },
     have hx' : 1 < (x : ℝ) := by exact_mod_cast hx,
-    have hxp : 0 < x := zero_lt_one.trans hx,
+    have hxp : 0 < x := by positivity,
     exact le_of_all_pow_lt_succ' hx' (f_pos_of_pos hxp H1 H4) hxnm1 },
 
   have h_f_commutes_with_pos_nat_mul : ∀ n : ℕ, 0 < n → ∀ x : ℚ, 0 < x → f (n * x) = n * f x,

src/analysis/convex/basic.lean

@@ -8,6 +8,7 @@ import algebra.order.module
 import linear_algebra.affine_space.midpoint
 import linear_algebra.affine_space.affine_subspace
 import linear_algebra.ray
+import tactic.positivity
 
 /-!
 # Convex sets and functions in vector spaces
@@ -331,8 +332,8 @@ begin
     use [a, b, ha, hb],
     rw [hab, div_one, div_one] },
   { rintro ⟨a, b, ha, hb, rfl⟩,
-    have hab : 0 < a + b, from add_pos ha hb,
-    refine ⟨a / (a + b), b / (a + b), div_pos ha hab, div_pos hb hab, _, rfl⟩,
+    have hab : 0 < a + b := by positivity,
+    refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, _, rfl⟩,
     rw [← add_div, div_self hab.ne'] }
 end
 
@@ -1005,9 +1006,9 @@ begin
     exact ⟨p • v, q • v, smul_mem_smul_set hv, smul_mem_smul_set hv, (add_smul _ _ _).symm⟩ },
   { rintro ⟨v₁, v₂, ⟨v₁₁, h₁₂, rfl⟩, ⟨v₂₁, h₂₂, rfl⟩, rfl⟩,
     have hpq := add_pos hp' hq',
-    exact mem_smul_set.2 ⟨_, h_conv h₁₂ h₂₂ (div_pos hp' hpq).le (div_pos hq' hpq).le
+    refine mem_smul_set.2 ⟨_, h_conv h₁₂ h₂₂ _ _
       (by rw [←div_self hpq.ne', add_div] : p / (p + q) + q / (p + q) = 1),
-      by simp only [← mul_smul, smul_add, mul_div_cancel' _ hpq.ne']⟩ }
+      by simp only [← mul_smul, smul_add, mul_div_cancel' _ hpq.ne']⟩; positivity }
 end
 
 end add_comm_group

src/analysis/mean_inequalities_pow.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne
 -/
 import analysis.convex.specific_functions
+import tactic.positivity
 
 /-!
 # Mean value inequalities
@@ -71,7 +72,7 @@ theorem arith_mean_le_rpow_mean (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
   (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) {p : ℝ} (hp : 1 ≤ p) :
   ∑ i in s, w i * z i ≤ (∑ i in s, (w i * z i ^ p)) ^ (1 / p) :=
 begin
-  have : 0 < p := lt_of_lt_of_le zero_lt_one hp,
+  have : 0 < p := by positivity,
   rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one],
   exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp,
   all_goals { apply_rules [sum_nonneg, rpow_nonneg_of_nonneg],
@@ -133,7 +134,7 @@ end
 lemma add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0) (hp1 : 1 ≤ p) :
   a ^ p + b ^ p ≤ (a + b) ^ p :=
 begin
-  have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1,
+  have hp_pos : 0 < p := by positivity,
   by_cases h_zero : a + b = 0,
   { simp [add_eq_zero_iff.mp h_zero, hp_pos.ne'] },
   have h_nonzero : ¬(a = 0 ∧ b = 0), by rwa add_eq_zero_iff at h_zero,
@@ -190,8 +191,8 @@ theorem rpow_arith_mean_le_arith_mean_rpow (w z : ι → ℝ≥0∞) (hw' : ∑
   (hp : 1 ≤ p) :
   (∑ i in s, w i * z i) ^ p ≤ ∑ i in s, (w i * z i ^ p) :=
 begin
-  have hp_pos : 0 < p, from lt_of_lt_of_le zero_lt_one hp,
-  have hp_nonneg : 0 ≤ p, from le_of_lt hp_pos,
+  have hp_pos : 0 < p, positivity,
+  have hp_nonneg : 0 ≤ p, positivity,
   have hp_not_nonpos : ¬ p ≤ 0, by simp [hp_pos],
   have hp_not_neg : ¬ p < 0, by simp [hp_nonneg],
   have h_top_iff_rpow_top : ∀ (i : ι) (hi : i ∈ s), w i * z i = ⊤ ↔ w i * (z i) ^ p = ⊤,
@@ -252,7 +253,7 @@ namespace ennreal
 lemma add_rpow_le_rpow_add {p : ℝ} (a b : ℝ≥0∞) (hp1 : 1 ≤ p) :
   a ^ p + b ^ p ≤ (a + b) ^ p :=
 begin
-  have hp_pos : 0 < p := lt_of_lt_of_le zero_lt_one hp1,
+  have hp_pos : 0 < p := by positivity,
   by_cases h_top : a + b = ⊤,
   { rw ←@ennreal.rpow_eq_top_iff_of_pos (a + b) p hp_pos at h_top,
     rw h_top,

src/topology/algebra/order/basic.lean

@@ -9,6 +9,7 @@ import order.filter.interval
 import topology.algebra.field
 import tactic.linarith
 import tactic.tfae
+import tactic.positivity
 
 /-!
 # Theory of topology on ordered spaces
@@ -1795,8 +1796,7 @@ section continuous_mul
 lemma mul_tendsto_nhds_zero_right (x : α) :
   tendsto (uncurry ((*) : α → α → α)) (𝓝 0 ×ᶠ 𝓝 x) $ 𝓝 0 :=
 begin
-  have hx : 0 < 2 * (1 + |x|) := (mul_pos (zero_lt_two) $
-    lt_of_lt_of_le zero_lt_one $ le_add_of_le_of_nonneg le_rfl (abs_nonneg x)),
+  have hx : 0 < 2 * (1 + |x|) := by positivity,
   rw ((nhds_basis_zero_abs_sub_lt α).prod $ nhds_basis_abs_sub_lt x).tendsto_iff
      (nhds_basis_zero_abs_sub_lt α),
   refine λ ε ε_pos, ⟨(ε/(2 * (1 + |x|)), 1), ⟨div_pos ε_pos hx, zero_lt_one⟩, _⟩,
@@ -1806,7 +1806,6 @@ begin
   refine lt_of_le_of_lt (mul_le_mul_of_nonneg_left _ (abs_nonneg a)) ((lt_div_iff hx).1 h),
   calc |b| = |(b - x) + x| : by rw sub_add_cancel b x
     ... ≤ |b - x| + |x| : abs_add (b - x) x
-    ... ≤ 1 + |x| : add_le_add_right (le_of_lt h') (|x|)
     ... ≤ 2 * (1 + |x|) : by linarith,
 end
 
@@ -1833,7 +1832,7 @@ begin
     refine ⟨i / (|x₀|), div_pos hi (abs_pos.2 hx₀), λ x hx, hit _⟩,
     calc |x₀ * x - x₀| = |x₀ * (x - 1)| : congr_arg abs (by ring_nf)
       ... = |x₀| * |x - 1| : abs_mul x₀ (x - 1)
-      ... < |x₀| * (i / |x₀|) : mul_lt_mul' le_rfl hx (abs_nonneg (x - 1)) (abs_pos.2 hx₀)
+      ... < |x₀| * (i / |x₀|) : mul_lt_mul' le_rfl hx (by positivity) (abs_pos.2 hx₀)
       ... = |x₀| * i / |x₀| : by ring
       ... = i : mul_div_cancel_left i (λ h, hx₀ (abs_eq_zero.1 h)) },
   { obtain ⟨i, hi, hit⟩ := h,
@@ -1842,8 +1841,7 @@ begin
     calc |x / x₀ - 1| = |x / x₀ - x₀ / x₀| : (by rw div_self hx₀)
     ... = |(x - x₀) / x₀| : congr_arg abs (sub_div x x₀ x₀).symm
     ... = |x - x₀| / |x₀| : abs_div (x - x₀) x₀
-    ... < i * |x₀| / |x₀| : div_lt_div hx le_rfl
-      (mul_nonneg (le_of_lt hi) (abs_nonneg x₀)) (abs_pos.2 hx₀)
+    ... < i * |x₀| / |x₀| : div_lt_div_of_lt (abs_pos.2 hx₀) hx
     ... = i : by rw [← mul_div_assoc', div_self (ne_of_lt $ abs_pos.2 hx₀).symm, mul_one],
     specialize hit (x / x₀) this,
     rwa [mul_div_assoc', mul_div_cancel_left x hx₀] at hit }
@@ -1869,7 +1867,7 @@ begin
   refine ⟨lt_of_le_of_lt _ (mul_lt_mul'' ha hb hε' hε'),
     lt_of_lt_of_le (mul_lt_mul'' ha' hb' ha0 hb0) _⟩,
   { calc 1 - ε = 1 - ε / 2 - ε/2 : by ring_nf
-    ... ≤ 1 - ε/2 - ε/2 + (ε/2)*(ε/2) : le_add_of_nonneg_right (le_of_lt (mul_pos ε_pos' ε_pos'))
+    ... ≤ 1 - ε/2 - ε/2 + (ε/2)*(ε/2) : le_add_of_nonneg_right (by positivity)
     ... = (1 - ε/2) * (1 - ε/2) : by ring_nf
     ... ≤ (1 - ε/4) * (1 - ε/4) : mul_le_mul (by linarith) (by linarith) (by linarith) hε' },
   { calc (1 + ε/4) * (1 + ε/4) = 1 + ε/2 + (ε/4)*(ε/4) : by ring_nf
@@ -1976,7 +1974,7 @@ by simpa only [mul_comm] using hg.at_bot_mul_neg hC hf
 lemma tendsto_inv_zero_at_top : tendsto (λx:α, x⁻¹) (𝓝[>] (0:α)) at_top :=
 begin
   refine (at_top_basis' 1).tendsto_right_iff.2 (λ b hb, _),
-  have hb' : 0 < b := zero_lt_one.trans_le hb,
+  have hb' : 0 < b := by positivity,
   filter_upwards [Ioc_mem_nhds_within_Ioi ⟨le_rfl, inv_pos.2 hb'⟩]
     with x hx using (le_inv hx.1 hb').1 hx.2,
 end
@@ -2073,18 +2071,17 @@ instance linear_ordered_field.to_topological_division_ring : topological_divisio
     rw [continuous_at,
         (nhds_basis_Ioo_pos t).tendsto_iff $ nhds_basis_Ioo_pos_of_pos $ inv_pos.2 ht],
     rintros ε ⟨hε : ε > 0, hεt : ε ≤ t⁻¹⟩,
-    refine ⟨min (t ^ 2 * ε / 2) (t / 2),
-            lt_min (half_pos $ mul_pos (by nlinarith) hε) $ by linarith, λ x h, _⟩,
+    refine ⟨min (t ^ 2 * ε / 2) (t / 2), by positivity, λ x h, _⟩,
     have hx : t / 2 < x,
     { rw [set.mem_Ioo, sub_lt, lt_min_iff] at h,
       nlinarith },
     have hx' : 0 < x := (half_pos ht).trans hx,
-    have aux : 0 < 2 / t ^ 2 := div_pos zero_lt_two (sq_pos_of_pos ht),
+    have aux : 0 < 2 / t ^ 2 := by positivity,
     rw [set.mem_Ioo, ←sub_lt_iff_lt_add', sub_lt, ←abs_sub_lt_iff] at h ⊢,
     rw [inv_sub_inv ht.ne' hx'.ne', abs_div, div_eq_mul_inv],
     suffices : |t * x|⁻¹ < 2 / t ^ 2,
     { rw [←abs_neg, neg_sub],
-      refine (mul_lt_mul'' h this (abs_nonneg _) $ inv_nonneg.mpr $ abs_nonneg _).trans_le _,
+      refine (mul_lt_mul'' h this (by positivity) (by positivity)).trans_le _,
       rw [mul_comm, mul_min_of_nonneg _ _ aux.le],
       apply min_le_of_left_le,
       rw [←mul_div, ←mul_assoc, div_mul_cancel _ (sq_pos_of_pos ht).ne',