[Merged by Bors] - feat: More rpow lemmas

Archive/Imo/Imo2001Q2.lean

@@ -67,7 +67,7 @@ open Imo2001Q2
 theorem imo2001_q2 (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : ↑1 ≤
     a / sqrt (a ^ 2 + ↑8 * b * c) + b / sqrt (b ^ 2 + ↑8 * c * a) + c / sqrt (c ^ 2 + ↑8 * a * b) :=
   have h3 : ∀ {x : ℝ}, 0 < x → (x ^ (3 : ℝ)⁻¹) ^ 3 = x := fun hx =>
-    show ↑3 = (3 : ℝ) by norm_num ▸ rpow_nat_inv_pow_nat hx.le three_ne_zero
+    show ↑3 = (3 : ℝ) by norm_num ▸ rpow_inv_natCast_pow hx.le three_ne_zero
   calc
     1 ≤ _ := imo2001_q2' (rpow_pos_of_pos ha _) (rpow_pos_of_pos hb _) (rpow_pos_of_pos hc _)
     _ = _ := by rw [h3 ha, h3 hb, h3 hc]

Mathlib/Analysis/SpecialFunctions/CompareExp.lean

@@ -136,7 +136,7 @@ theorem isLittleO_log_abs_re (hl : IsExpCmpFilter l) : (fun z => Real.log (abs z
           have hm₀ : 0 < max z.re |z.im| := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
           rw [one_mul, Real.norm_eq_abs, _root_.abs_of_nonneg (Real.log_nonneg hz')]
           refine' le_trans _ (le_abs_self _)
-          rw [← Real.log_mul, Real.log_le_log, ← _root_.abs_of_nonneg (le_trans zero_le_one hz)]
+          rw [← Real.log_mul, Real.log_le_log_iff, ← _root_.abs_of_nonneg (le_trans zero_le_one hz)]
           exacts [abs_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne']
     _ =o[l] re :=
       IsLittleO.add (isLittleO_const_left.2 <| Or.inr <| hl.tendsto_abs_re) <|

Mathlib/Analysis/SpecialFunctions/Log/Base.lean

@@ -182,7 +182,7 @@ private theorem b_ne_one' : b ≠ 1 := by linarith
 
 @[simp]
 theorem logb_le_logb (h : 0 < x) (h₁ : 0 < y) : logb b x ≤ logb b y ↔ x ≤ y := by
-  rw [logb, logb, div_le_div_right (log_pos hb), log_le_log h h₁]
+  rw [logb, logb, div_le_div_right (log_pos hb), log_le_log_iff h h₁]
 #align real.logb_le_logb Real.logb_le_logb
 
 @[gcongr]
@@ -295,7 +295,7 @@ private theorem b_ne_one : b ≠ 1 := by linarith
 
 @[simp]
 theorem logb_le_logb_of_base_lt_one (h : 0 < x) (h₁ : 0 < y) : logb b x ≤ logb b y ↔ y ≤ x := by
-  rw [logb, logb, div_le_div_right_of_neg (log_neg b_pos b_lt_one), log_le_log h₁ h]
+  rw [logb, logb, div_le_div_right_of_neg (log_neg b_pos b_lt_one), log_le_log_iff h₁ h]
 #align real.logb_le_logb_of_base_lt_one Real.logb_le_logb_of_base_lt_one
 
 theorem logb_lt_logb_of_base_lt_one (hx : 0 < x) (hxy : x < y) : logb b y < logb b x := by

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -141,22 +141,18 @@ theorem log_inv (x : ℝ) : log x⁻¹ = -log x := by
   rw [← exp_eq_exp, exp_log_eq_abs (inv_ne_zero hx), exp_neg, exp_log_eq_abs hx, abs_inv]
 #align real.log_inv Real.log_inv
 
-theorem log_le_log (h : 0 < x) (h₁ : 0 < y) : log x ≤ log y ↔ x ≤ y := by
+theorem log_le_log_iff (h : 0 < x) (h₁ : 0 < y) : log x ≤ log y ↔ x ≤ y := by
   rw [← exp_le_exp, exp_log h, exp_log h₁]
-#align real.log_le_log Real.log_le_log
+#align real.log_le_log Real.log_le_log_iff
 
 @[gcongr]
-theorem log_lt_log (hx : 0 < x) : x < y → log x < log y := by
-  intro h
-  rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]
-#align real.log_lt_log Real.log_lt_log
+lemma log_le_log (hx : 0 < x) (hxy : x ≤ y) : log x ≤ log y :=
+  (log_le_log_iff hx (hx.trans_le hxy)).2 hxy
 
 @[gcongr]
-theorem log_le_log' (hx : 0 < x) : x ≤ y → log x ≤ log y := by
-  intro hxy
-  cases hxy.eq_or_lt with
-  | inl h_eq => simp [h_eq]
-  | inr hlt => exact le_of_lt <| log_lt_log hx hlt
+theorem log_lt_log (hx : 0 < x) (h : x < y) : log x < log y := by
+  rwa [← exp_lt_exp, exp_log hx, exp_log (lt_trans hx h)]
+#align real.log_lt_log Real.log_lt_log
 
 theorem log_lt_log_iff (hx : 0 < x) (hy : 0 < y) : log x < log y ↔ x < y := by
   rw [← exp_lt_exp, exp_log hx, exp_log hy]

Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

@@ -320,15 +320,15 @@ theorem rpow_one_div_eq_iff {x y : ℝ≥0} {z : ℝ} (hz : z ≠ 0) : x ^ (1 /
   rw [← rpow_eq_rpow_iff hz, rpow_self_rpow_inv hz]
 #align nnreal.rpow_one_div_eq_iff NNReal.rpow_one_div_eq_iff
 
-theorem pow_nat_rpow_nat_inv (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ n) ^ (n⁻¹ : ℝ) = x := by
+theorem pow_rpow_inv_natCast (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ n) ^ (n⁻¹ : ℝ) = x := by
   rw [← NNReal.coe_eq, coe_rpow, NNReal.coe_pow]
-  exact Real.pow_nat_rpow_nat_inv x.2 hn
-#align nnreal.pow_nat_rpow_nat_inv NNReal.pow_nat_rpow_nat_inv
+  exact Real.pow_rpow_inv_natCast x.2 hn
+#align nnreal.pow_nat_rpow_nat_inv NNReal.pow_rpow_inv_natCast
 
-theorem rpow_nat_inv_pow_nat (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ (n⁻¹ : ℝ)) ^ n = x := by
+theorem rpow_inv_natCast_pow (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ (n⁻¹ : ℝ)) ^ n = x := by
   rw [← NNReal.coe_eq, NNReal.coe_pow, coe_rpow]
-  exact Real.rpow_nat_inv_pow_nat x.2 hn
-#align nnreal.rpow_nat_inv_pow_nat NNReal.rpow_nat_inv_pow_nat
+  exact Real.rpow_inv_natCast_pow x.2 hn
+#align nnreal.rpow_nat_inv_pow_nat NNReal.rpow_inv_natCast_pow
 
 theorem _root_.Real.toNNReal_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) :
     Real.toNNReal (x ^ y) = Real.toNNReal x ^ y := by