chore: golf using positivity (#37554)

Author: grunweg

Mathlib/Analysis/MeanInequalities.lean

@@ -357,7 +357,7 @@ theorem harm_mean_le_geom_mean_weighted (w z : ι → ℝ) (hs : s.Nonempty) (hw
     inv_pos.2 (prod_pos fun i hi => rpow_pos_of_pos ((hz i hi)) _)
   rw [← inv_inv (∏ i ∈ s, z i ^ w i), inv_le_inv₀ p_pos p_pos₂, ← Finset.prod_inv_distrib]
   gcongr
-  · exact fun i hi ↦ inv_nonneg.mpr (Real.rpow_nonneg (le_of_lt (hz i hi)) _)
+  · exact fun i hi ↦ by positivity [hz i hi]
   · rw [Real.inv_rpow]; apply fun i hi ↦ le_of_lt (hz i hi); assumption
 
 
@@ -371,7 +371,7 @@ theorem harm_mean_le_geom_mean {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (w
     nth_rw 1 [div_eq_mul_inv, (show n = (n⁻¹)⁻¹ by simp), ← mul_inv, Finset.mul_sum _ _ n⁻¹]
     simp_rw [inv_mul_eq_div n ((w _) / (z _)), div_right_comm _ _ n]
     convert this
-    rw [← Real.finset_prod_rpow s _ (fun i hi ↦ Real.rpow_nonneg (le_of_lt <| hz i hi) _)]
+    rw [← Real.finset_prod_rpow s _ (fun i hi ↦ by positivity [hz i hi])]
     refine Finset.prod_congr rfl (fun i hi => ?_)
     rw [← Real.rpow_mul (le_of_lt <| hz i hi) (w _) n⁻¹, div_eq_mul_inv (w _) n]
   · exact fun i hi ↦ div_pos (hw i hi) hw'

Mathlib/Analysis/MellinTransform.lean

@@ -250,11 +250,11 @@ theorem mellin_convergent_zero_of_isBigO {b : ℝ} {f : ℝ → ℝ}
     · refine (ae_restrict_iff' measurableSet_Ioo).mpr (Eventually.of_forall fun t ht => ?_)
       rw [mul_comm, norm_mul]
       specialize hε' _ ht.1
-      · rw [dist_eq_norm, sub_zero, norm_of_nonneg (le_of_lt ht.1)]
+      · rw [dist_eq_norm, sub_zero, norm_of_nonneg ht.1.le]
         exact ht.2
       · calc _ ≤ d * ‖t ^ (-b)‖ * ‖t ^ (s - 1)‖ := by gcongr
           _ = d * t ^ (s - b - 1) := ?_
-        simp_rw [norm_of_nonneg (rpow_nonneg (le_of_lt ht.1) _), mul_assoc]
+        simp_rw [norm_of_nonneg (rpow_nonneg ht.1.le _), mul_assoc]
         rw [← rpow_add ht.1]
         congr 2
         abel

Mathlib/Analysis/Normed/Lp/lpSpace.lean

@@ -115,7 +115,7 @@ theorem memℓp_gen' {C : ℝ} {f : ∀ i, E i} (hf : ∀ s : Finset α, ∑ i 
   use ⨆ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal
   apply hasSum_of_isLUB_of_nonneg
   · intro b
-    exact Real.rpow_nonneg (norm_nonneg _) _
+    positivity
   apply isLUB_ciSup
   use C
   rintro - ⟨s, rfl⟩
@@ -239,7 +239,7 @@ theorem of_exponent_ge {p q : ℝ≥0∞} {f : ∀ i, E i} (hfq : Memℓp f q) (
       exact H.subset fun i hi => Real.one_le_rpow hi hq.le
     · change ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖
       intro i hi
-      have : 0 ≤ ‖f i‖ ^ p.toReal := Real.rpow_nonneg (norm_nonneg _) p.toReal
+      have : 0 ≤ ‖f i‖ ^ p.toReal := by positivity
       simp only [abs_of_nonneg, this] at hi
       contrapose! hi
       exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'
@@ -472,8 +472,7 @@ theorem norm_nonneg' (f : lp E p) : 0 ≤ ‖f‖ := by
     inhabit α
     exact (norm_nonneg (f default)).trans ((lp.isLUB_norm f).1 ⟨default, rfl⟩)
   · rw [lp.norm_eq_tsum_rpow hp f]
-    refine Real.rpow_nonneg (tsum_nonneg ?_) _
-    exact fun i => Real.rpow_nonneg (norm_nonneg _) _
+    exact Real.rpow_nonneg (tsum_nonneg fun i ↦ by positivity) _
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
@@ -501,7 +500,7 @@ theorem norm_eq_zero_iff {f : lp E p} : ‖f‖ = 0 ↔ f = 0 := by
   · have hf : HasSum (fun i : α => ‖f i‖ ^ p.toReal) 0 := by
       have := lp.hasSum_norm hp f
       rwa [h, Real.zero_rpow hp.ne'] at this
-    have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _
+    have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity
     rw [hasSum_zero_iff_of_nonneg this] at hf
     ext i
     have : f i = 0 ∧ p.toReal ≠ 0 := by
@@ -584,7 +583,7 @@ theorem norm_apply_le_norm (hp : p ≠ 0) (f : lp E p) (i : α) : ‖f i‖ ≤
   · haveI : Nonempty α := ⟨i⟩
     exact (isLUB_norm f).1 ⟨i, rfl⟩
   have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp hp'
-  have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _
+  have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity
   rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) hp'']
   convert le_hasSum (hasSum_norm hp'' f) i fun i _ => this i
 
@@ -597,7 +596,7 @@ lemma lipschitzWith_one_eval (p : ℝ≥0∞) [Fact (1 ≤ p)] (i : α) :
 theorem sum_rpow_le_norm_rpow (hp : 0 < p.toReal) (f : lp E p) (s : Finset α) :
     ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal := by
   rw [lp.norm_rpow_eq_tsum hp f]
-  have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i => Real.rpow_nonneg (norm_nonneg _) _
+  have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ by positivity
   refine Summable.sum_le_tsum _ (fun i _ => this i) ?_
   exact (lp.memℓp f).summable hp
 

Mathlib/Analysis/Normed/Unbundled/IsPowMulFaithful.lean

@@ -47,9 +47,8 @@ theorem contraction_of_isPowMul_of_boundedWrt {F : Type*} {α : outParam (Type*)
   intro n hn
   have h : (C ^ (1 / n : ℝ)) ^ n = C := by
     have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (ne_of_gt hn)
-    rw [← rpow_natCast, ← rpow_mul (le_of_lt hC0), one_div, inv_mul_cancel₀ hn0, rpow_one]
-  apply le_of_pow_le_pow_left₀ (ne_of_gt hn)
-    (mul_nonneg (rpow_nonneg (le_of_lt hC0) _) (apply_nonneg _ _))
+    rw [← rpow_natCast, ← rpow_mul hC0.le, one_div, inv_mul_cancel₀ hn0, rpow_one]
+  apply le_of_pow_le_pow_left₀ (ne_of_gt hn) (by positivity)
   · rw [mul_pow, h, ← hβ _ hn, ← map_pow]
     apply le_trans (hC (x ^ n))
     rw [mul_le_mul_iff_right₀ hC0]

Mathlib/Analysis/Normed/Unbundled/SmoothingSeminorm.lean

@@ -88,7 +88,7 @@ private theorem smoothingSeminormSeq_tendsto_aux {L : ℝ} (hL : 0 ≤ L) {ε :
 theorem zero_mem_lowerBounds_smoothingSeminormSeq_range (x : R) :
     0 ∈ lowerBounds (Set.range fun n : ℕ+ => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))) := by
   rintro y ⟨n, rfl⟩
-  exact rpow_nonneg (apply_nonneg μ _) _
+  positivity
 
 /-- `smoothingSeminormSeq` is bounded below (by zero). -/
 theorem smoothingSeminormSeq_bddBelow (x : R) :
@@ -111,15 +111,15 @@ theorem tendsto_smoothingFun_of_eq_zero {x : R} (hx : μ x = 0) :
   have hL0 : (iInf fun n : PNat => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))) = 0 :=
     le_antisymm
       (ciInf_le_of_le (smoothingSeminormSeq_bddBelow μ x) (1 : PNat) (le_of_eq (h0 1 (le_refl _))))
-      (le_ciInf fun n => rpow_nonneg (apply_nonneg μ _) _)
+      (le_ciInf fun n ↦ by positivity)
   simpa only [hL0] using tendsto_atTop_of_eventually_const h0
 
 /-- If `μ 1 ≤ 1` and `μ x ≠ 0`, then `smoothingFun μ x` is the limit of
 `smoothingSeminormSeq μ x`. -/
 theorem tendsto_smoothingFun_of_ne_zero (hμ1 : μ 1 ≤ 1) {x : R} (hx : μ x ≠ 0) :
     Tendsto (smoothingSeminormSeq μ x) atTop (𝓝 (smoothingFun μ x)) := by
   let L := iInf fun n : PNat => μ (x ^ (n : ℕ)) ^ (1 / (n : ℝ))
-  have hL0 : 0 ≤ L := le_ciInf fun x => rpow_nonneg (apply_nonneg _ _) _
+  have hL0 : 0 ≤ L := le_ciInf fun x ↦ by positivity
   rw [Metric.tendsto_atTop]
   intro ε hε
   /- For each `ε > 0`, we can find a positive natural number `m1` such that
@@ -247,7 +247,7 @@ theorem tendsto_smoothingFun_of_map_one_le_one (hμ1 : μ 1 ≤ 1) (x : R) :
 /-- If `μ 1 ≤ 1`, then `smoothingFun μ x` is nonnegative. -/
 theorem smoothingFun_nonneg (hμ1 : μ 1 ≤ 1) (x : R) : 0 ≤ smoothingFun μ x := by
   apply ge_of_tendsto (tendsto_smoothingFun_of_map_one_le_one μ hμ1 x)
-  simpa [eventually_atTop, ge_iff_le] using ⟨1, fun _ _ ↦ rpow_nonneg (apply_nonneg μ _) _⟩
+  simpa [eventually_atTop, ge_iff_le] using ⟨1, fun _ _ ↦ by positivity⟩
 
 /-- If `μ 1 ≤ 1`, then `smoothingFun μ 1 ≤ 1`. -/
 theorem smoothingFun_one_le (hμ1 : μ 1 ≤ 1) : smoothingFun μ 1 ≤ 1 := by
@@ -398,7 +398,7 @@ private theorem limsup_mu_le (hμ1 : μ 1 ≤ 1) {s : ℕ → ℕ} (hs_le : ∀
           · use 0
             simp only [mem_lowerBounds, eventually_map, eventually_atTop, ge_iff_le,
               Set.mem_setOf_eq, forall_exists_index]
-            exact fun _ m hm ↦ le_trans (rpow_nonneg (apply_nonneg μ _) _) (hm m (le_refl _))
+            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))
       _ ≤ 1 := (μ_limsup_le_one μ hs_le hψ_lim)
       _ = smoothingFun μ x ^ a := by rw [ha, rpow_zero]
   · have ha_pos : 0 < a := lt_of_le_of_ne a_in.1 (Ne.symm ha)
@@ -465,15 +465,14 @@ theorem isNonarchimedean_smoothingFun (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedea
       limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)))
         atTop ≤ limsup (fun n : ℕ => μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop *
           limsup (fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ))) atTop :=
-      limsup_mul_le (Frequently.of_forall (fun n => rpow_nonneg (apply_nonneg _ _) _))
+      limsup_mul_le (Frequently.of_forall (fun n ↦ by positivity))
         (μ_bddAbove μ hμ1 hmu_le x ψ).isBoundedUnder_of_range
-        (Eventually.of_forall (fun n => rpow_nonneg (apply_nonneg _ _) _))
+        (Eventually.of_forall (fun n ↦ by positivity))
         (μ_bddAbove μ hμ1 hnu_le y ψ).isBoundedUnder_of_range
     have h_bdd : IsBoundedUnder LE.le atTop fun n : ℕ => μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)) :=
       RingSeminorm.isBoundedUnder μ hμ1 hnu_le ψ
     apply le_trans hxy' (mul_le_mul hx hy (le_limsup_of_frequently_le (Frequently.of_forall
-      (fun n ↦ rpow_nonneg (apply_nonneg μ _) _)) h_bdd)
-        (rpow_nonneg (smoothingFun_nonneg μ hμ1 x) _))
+      (fun n ↦ by positivity)) h_bdd) (rpow_nonneg (smoothingFun_nonneg μ hμ1 x) _))
   apply le_of_forall_sub_le
   /- Fix `ε > 0`. We first show that `smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε ≤
     max (smoothingFun μ x) (smoothingFun μ y) + ε`. -/
@@ -502,8 +501,8 @@ theorem isNonarchimedean_smoothingFun (hμ1 : μ 1 ≤ 1) (hna : IsNonarchimedea
   have hex : ∃ n : PNat, μ (x ^ mu (ψ n)) ^ (1 / (ψ n : ℝ)) * μ (y ^ nu (ψ n)) ^ (1 / (ψ n : ℝ)) <
       smoothingFun μ x ^ a * smoothingFun μ y ^ b + ε :=
     Filter.exists_lt_of_limsup_le (bddAbove_range_mul (μ_bddAbove μ hμ1 hmu_le _ _)
-      (fun n => rpow_nonneg (apply_nonneg _ _) _) (μ_bddAbove μ hμ1 hnu_le _ _)
-        fun n => rpow_nonneg (apply_nonneg _ _) _).isBoundedUnder_of_range hxy hε
+      (fun n ↦ by positivity) (μ_bddAbove μ hμ1 hnu_le _ _)
+      (fun n ↦ by positivity)).isBoundedUnder_of_range hxy hε
   obtain ⟨N, hN⟩ := hex
   /- By definition of `smoothingFun`, and applying the inequality `hN`, it suffices to show that
     `μ ((x + y) ^ ψ N) ^ (1 / ψ N) ≤ μ (x ^ mu (ψ N)) ^ (1 / ψ N) * μ (y ^ nu ψ N) ^ (1 / ψ N)`. -/

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

@@ -129,7 +129,7 @@ theorem spectralValueTerms_bddAbove (p : R[X]) : BddAbove (Set.range (spectralVa
 theorem spectralValueTerms_nonneg (p : R[X]) (n : ℕ) : 0 ≤ spectralValueTerms p n := by
   simp only [spectralValueTerms]
   split_ifs with h
-  · exact rpow_nonneg (norm_nonneg _) _
+  · positivity
   · exact le_refl _
 
 /-- The spectral value of a polynomial is nonnegative. -/
@@ -262,7 +262,8 @@ theorem norm_root_le_spectralValue {f : AlgebraNorm K L} (hf_pm : IsPowMul f)
           Set.range (spectralValueTerms p) := by use n; simp only [spectralValueTerms, if_pos hn]
         exact h_ge (‖p.coeff n‖₊ ^ (1 / (p.natDegree - n : ℝ))) h_rg
       rw [← hexp, ← rpow_natCast, ← rpow_natCast]
-      exact rpow_lt_rpow (rpow_nonneg (norm_nonneg _) _) h_base (cast_pos.mpr (tsub_pos_of_lt hn))
+      gcongr
+      exact cast_pos.mpr (tsub_pos_of_lt hn)
     have h_deg : 0 < p.natDegree := natDegree_pos_of_monic_of_aeval_eq_zero hp hx
     have h_lt : f ((Finset.range p.natDegree).sum fun i : ℕ ↦ p.coeff i • x ^ i) <
         f (x ^ p.natDegree) := by

Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean

@@ -327,7 +327,7 @@ theorem approx_Gamma_integral_tendsto_Gamma_integral {s : ℂ} (hs : 0 < re s) :
     rcases lt_or_ge (n : ℝ) x with (hxn | hxn)
     · rw [indicator_of_notMem (notMem_Ioc_of_gt hxn), norm_zero,
         mul_nonneg_iff_right_nonneg_of_pos (exp_pos _)]
-      exact rpow_nonneg (le_of_lt hx) _
+      positivity
     · rw [indicator_of_mem (mem_Ioc.mpr ⟨mem_Ioi.mp hx, hxn⟩), norm_mul, Complex.norm_of_nonneg
           (pow_nonneg (sub_nonneg.mpr <| div_le_one_of_le₀ hxn <| by positivity) _),
           norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]

Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

@@ -388,7 +388,7 @@ theorem le_N (hN : 2 ≤ N) : (2 * dValue N - 1) ^ nValue N ≤ N := by
     rw [cast_ne_zero]
     apply (nValue_pos hN).ne'
   rw [← le_div_iff₀']
-  · exact floor_le (div_nonneg (rpow_nonneg (cast_nonneg _) _) zero_le_two)
+  · exact floor_le (by positivity)
   apply zero_lt_two
 
 theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dValue N := by

Mathlib/MeasureTheory/Function/UniformIntegrable.lean

@@ -290,7 +290,7 @@ theorem MemLp.eLpNorm_indicator_norm_ge_le (hf : MemLp f p μ) (hmeas : Strongly
   rw [enorm_indicator_eq_indicator_enorm, enorm_indicator_eq_indicator_enorm]
   have hiff : M ^ (1 / p.toReal) ≤ ‖f x‖₊ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖₊ := by
     rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
-      ← Real.rpow_le_rpow_iff hM' (Real.rpow_nonneg (norm_nonneg _) _)
+      ← Real.rpow_le_rpow_iff hM' (by positivity)
         (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
       mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
   by_cases hx : x ∈ { x : α | M ^ (1 / p.toReal) ≤ ‖f x‖₊ }

Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

@@ -1183,11 +1183,11 @@ theorem integral_mul_norm_le_Lp_mul_Lq {E} [NormedAddCommGroup E] {f g : α →
   rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae,
     integral_eq_lintegral_of_nonneg_ae]
   rotate_left
-  · exact Eventually.of_forall fun x => Real.rpow_nonneg (norm_nonneg _) _
+  · exact Eventually.of_forall fun x ↦ by positivity
   · exact (hg.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable
-  · exact Eventually.of_forall fun x => Real.rpow_nonneg (norm_nonneg _) _
+  · exact Eventually.of_forall fun x ↦ by positivity
   · exact (hf.1.norm.aemeasurable.pow aemeasurable_const).aestronglyMeasurable
-  · exact Eventually.of_forall fun x => mul_nonneg (norm_nonneg _) (norm_nonneg _)
+  · exact Eventually.of_forall fun x ↦ by positivity
   · exact hf.1.norm.mul hg.1.norm
   rw [ENNReal.toReal_rpow, ENNReal.toReal_rpow, ← ENNReal.toReal_mul]
   -- replace norms by nnnorm