chore: Rename pow monotonicity lemmas (#9095)

The names for lemmas about monotonicity of `(a ^ ·)` and `(· ^ n)` were a mess. This PR tidies up everything related by following the naming convention for `(a * ·)` and `(· * b)`. Namely, `(a ^ ·)` is `pow_right` and `(· ^ n)` is `pow_left` in lemma names. All lemma renames follow the corresponding multiplication lemma names closely.

## Renames

### `Algebra.GroupPower.Order`

* `pow_mono` → `pow_right_mono`
* `pow_le_pow` → `pow_le_pow_right`
* `pow_le_pow_of_le_left` → `pow_le_pow_left`
* `pow_lt_pow_of_lt_left` → `pow_lt_pow_left`
* `strictMonoOn_pow` → `pow_left_strictMonoOn`
* `pow_strictMono_right` → `pow_right_strictMono`
* `pow_lt_pow` → `pow_lt_pow_right`
* `pow_lt_pow_iff` → `pow_lt_pow_iff_right`
* `pow_le_pow_iff` → `pow_le_pow_iff_right`
* `self_lt_pow` → `lt_self_pow`
* `strictAnti_pow` → `pow_right_strictAnti`
* `pow_lt_pow_iff_of_lt_one` → `pow_lt_pow_iff_right_of_lt_one`
* `pow_lt_pow_of_lt_one` → `pow_lt_pow_right_of_lt_one`
* `lt_of_pow_lt_pow` → `lt_of_pow_lt_pow_left`
* `le_of_pow_le_pow` → `le_of_pow_le_pow_left`
* `pow_lt_pow₀` → `pow_lt_pow_right₀`

### `Algebra.GroupPower.CovariantClass`

* `pow_le_pow_of_le_left'` → `pow_le_pow_left'`
* `nsmul_le_nsmul_of_le_right` → `nsmul_le_nsmul_right`
* `pow_lt_pow'` → `pow_lt_pow_right'`
* `nsmul_lt_nsmul` → `nsmul_lt_nsmul_left`
* `pow_strictMono_left` → `pow_right_strictMono'`
* `nsmul_strictMono_right` → `nsmul_left_strictMono`
* `StrictMono.pow_right'` → `StrictMono.pow_const`
* `StrictMono.nsmul_left` → `StrictMono.const_nsmul`
* `pow_strictMono_right'` → `pow_left_strictMono`
* `nsmul_strictMono_left` → `nsmul_right_strictMono`
* `Monotone.pow_right` → `Monotone.pow_const`
* `Monotone.nsmul_left` → `Monotone.const_nsmul`
* `lt_of_pow_lt_pow'` → `lt_of_pow_lt_pow_left'`
* `lt_of_nsmul_lt_nsmul` → `lt_of_nsmul_lt_nsmul_right`
* `pow_le_pow'` → `pow_le_pow_right'`
* `nsmul_le_nsmul` → `nsmul_le_nsmul_left`
* `pow_le_pow_of_le_one'` → `pow_le_pow_right_of_le_one'`
* `nsmul_le_nsmul_of_nonpos` → `nsmul_le_nsmul_left_of_nonpos`
* `le_of_pow_le_pow'` → `le_of_pow_le_pow_left'`
* `le_of_nsmul_le_nsmul'` → `le_of_nsmul_le_nsmul_right'`
* `pow_le_pow_iff'` → `pow_le_pow_iff_right'`
* `nsmul_le_nsmul_iff` → `nsmul_le_nsmul_iff_left`
* `pow_lt_pow_iff'` → `pow_lt_pow_iff_right'`
* `nsmul_lt_nsmul_iff` → `nsmul_lt_nsmul_iff_left`

### `Data.Nat.Pow`

* `Nat.pow_lt_pow_of_lt_left` → `Nat.pow_lt_pow_left`
* `Nat.pow_le_iff_le_left` → `Nat.pow_le_pow_iff_left`
* `Nat.pow_lt_iff_lt_left` → `Nat.pow_lt_pow_iff_left`

## Lemmas added

* `pow_le_pow_iff_left`
* `pow_lt_pow_iff_left`
* `pow_right_injective`
* `pow_right_inj`
* `Nat.pow_le_pow_left` to have the correct name since `Nat.pow_le_pow_of_le_left` is in Std.
* `Nat.pow_le_pow_right` to have the correct name since `Nat.pow_le_pow_of_le_right` is in Std.

## Lemmas removed

* `self_le_pow` was a duplicate of `le_self_pow`.
* `Nat.pow_lt_pow_of_lt_right` is defeq to `pow_lt_pow_right`.
* `Nat.pow_right_strictMono` is defeq to `pow_right_strictMono`.
* `Nat.pow_le_iff_le_right` is defeq to `pow_le_pow_iff_right`.
* `Nat.pow_lt_iff_lt_right` is defeq to `pow_lt_pow_iff_right`.

## Other changes

* A bunch of proofs have been golfed.
* Some lemma assumptions have been turned from `0 < n` or `1 ≤ n` to `n ≠ 0`.
* A few `Nat` lemmas have been `protected`.
* One docstring has been fixed.

Archive/Imo/Imo1962Q1.lean

@@ -117,11 +117,10 @@ theorem case_more_digits {c n : ℕ} (h1 : (digits 10 c).length ≥ 6) (h2 : Pro
     intro h4
     have h5 : (digits 10 c).length = 0 := by simp [h4]
     exact case_0_digit h5 h2
-  have h6 : 2 ≤ 10 := by decide
   calc
     n ≥ 10 * c := le.intro h2.left.symm
-    _ ≥ 10 ^ (digits 10 c).length := (base_pow_length_digits_le 10 c h6 h3)
-    _ ≥ 10 ^ 6 := ((pow_le_iff_le_right h6).mpr h1)
+    _ ≥ 10 ^ (digits 10 c).length := (base_pow_length_digits_le 10 c (by decide) h3)
+    _ ≥ 10 ^ 6 := pow_le_pow_right (by decide) h1
     _ ≥ 153846 := by norm_num
 #align imo1962_q1.case_more_digits Imo1962Q1.case_more_digits
 

Archive/Imo/Imo1969Q1.lean

@@ -86,7 +86,7 @@ theorem aChoice_good (b : ℕ) : aChoice b ∈ goodNats :=
 /-- `aChoice` is a strictly monotone function; this is easily proven by chaining together lemmas
 in the `strictMono` namespace. -/
 theorem aChoice_strictMono : StrictMono aChoice :=
-  ((strictMono_id.const_add 2).nat_pow (by decide : 0 < 4)).const_mul (by decide : 0 < 4)
+  ((strictMono_id.const_add 2).nat_pow (by decide)).const_mul (by decide)
 #align imo1969_q1.a_choice_strict_mono Imo1969Q1.aChoice_strictMono
 
 end Imo1969Q1

Archive/Imo/Imo2001Q2.lean

@@ -41,7 +41,7 @@ theorem bound (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
       = a ^ 3 * (a * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)) := by ring
     _ ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4) := ?_
   gcongr
-  apply le_of_pow_le_pow _ (by positivity) zero_lt_two
+  apply le_of_pow_le_pow_left two_ne_zero (by positivity)
   rw [mul_pow, sq_sqrt (by positivity), ← sub_nonneg]
   calc
     (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)

Archive/Imo/Imo2006Q3.lean

@@ -71,7 +71,7 @@ theorem subst_wlog {x y z s : ℝ} (hxy : 0 ≤ x * y) (hxyz : x + y + z = 0) :
       _ ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4 := by
           gcongr (?_ + _) ^ 4 / _
           apply rhs_ineq
-  refine le_of_pow_le_pow 2 (by positivity) (by positivity) ?_
+  refine le_of_pow_le_pow_left two_ne_zero (by positivity) ?_
   calc
     (32 * |x * y * z * s|) ^ 2 = 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2)) := by
       rw [mul_pow, sq_abs, hz]; ring

Archive/Imo/Imo2008Q3.lean

@@ -62,10 +62,10 @@ theorem p_lemma (p : ℕ) (hpp : Nat.Prime p) (hp_mod_4_eq_1 : p ≡ 1 [MOD 4])
   have hreal₂ : (p : ℝ) > 20 := by assumption_mod_cast
   have hreal₃ : (k : ℝ) ^ 2 + 4 ≥ p := by assumption_mod_cast
   have hreal₅ : (k : ℝ) > 4 := by
-    refine' lt_of_pow_lt_pow 2 k.cast_nonneg _
+    refine' lt_of_pow_lt_pow_left 2 k.cast_nonneg _
     linarith only [hreal₂, hreal₃]
   have hreal₆ : (k : ℝ) > sqrt (2 * n) := by
-    refine' lt_of_pow_lt_pow 2 k.cast_nonneg _
+    refine' lt_of_pow_lt_pow_left 2 k.cast_nonneg _
     rw [sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg)]
     linarith only [hreal₁, hreal₃, hreal₅]
   exact ⟨n, hnat₁, by linarith only [hreal₆, hreal₁]⟩

Archive/Imo/Imo2008Q4.lean

@@ -29,8 +29,7 @@ open Real
 namespace Imo2008Q4
 
 theorem abs_eq_one_of_pow_eq_one (x : ℝ) (n : ℕ) (hn : n ≠ 0) (h : x ^ n = 1) : |x| = 1 := by
-  rw [← pow_left_inj (abs_nonneg x) zero_le_one (pos_iff_ne_zero.2 hn), one_pow, pow_abs, h,
-    abs_one]
+  rw [← pow_left_inj (abs_nonneg x) zero_le_one hn, one_pow, pow_abs, h, abs_one]
 #align imo2008_q4.abs_eq_one_of_pow_eq_one Imo2008Q4.abs_eq_one_of_pow_eq_one
 
 end Imo2008Q4

Archive/Wiedijk100Theorems/AbelRuffini.lean

@@ -126,7 +126,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
     have hfa : 0 ≤ f a := by
       -- Porting note: was `simp_rw`
       simp only [hf, ← sq]
-      refine' add_nonneg (sub_nonneg.mpr (pow_le_pow ha _)) _ <;> norm_num
+      refine' add_nonneg (sub_nonneg.mpr (pow_le_pow_right ha _)) _ <;> norm_num
     obtain ⟨x, ⟨-, hx1⟩, hx2⟩ := intermediate_value_Ico' hle (hc _) (Set.mem_Ioc.mpr ⟨hf1, hf0⟩)
     obtain ⟨y, ⟨hy1, -⟩, hy2⟩ := intermediate_value_Ioc ha (hc _) (Set.mem_Ioc.mpr ⟨hf1, hfa⟩)
     exact ⟨x, y, (hx1.trans hy1).ne, hx2, hy2⟩
@@ -137,7 +137,7 @@ theorem real_roots_Phi_ge_aux (hab : b < a) :
         f (-a) = (a : ℝ) ^ 2 - (a : ℝ) ^ 5 + b := by
           norm_num [hf, ← sq, sub_eq_add_neg, add_comm, Odd.neg_pow (by decide : Odd 5)]
         _ ≤ (a : ℝ) ^ 2 - (a : ℝ) ^ 3 + (a - 1) := by
-          refine' add_le_add (sub_le_sub_left (pow_le_pow ha _) _) _ <;> linarith
+          refine' add_le_add (sub_le_sub_left (pow_le_pow_right ha _) _) _ <;> linarith
         _ = -((a : ℝ) - 1) ^ 2 * (a + 1) := by ring
         _ ≤ 0 := by nlinarith
     have ha' := neg_nonpos.mpr (hle.trans ha)

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -115,7 +115,7 @@ theorem eq_two_pow_mul_prime_mersenne_of_even_perfect {n : ℕ} (ev : Even n) (p
       | .succ k =>
         apply ne_of_lt _ jcon2
         rw [mersenne, ← Nat.pred_eq_sub_one, Nat.lt_pred_iff, ← pow_one (Nat.succ 1)]
-        apply pow_lt_pow (Nat.lt_succ_self 1) (Nat.succ_lt_succ (Nat.succ_pos k))
+        apply pow_lt_pow_right (Nat.lt_succ_self 1) (Nat.succ_lt_succ (Nat.succ_pos k))
     contrapose! hm
     simp [hm]
 #align theorems_100.nat.eq_two_pow_mul_prime_mersenne_of_even_perfect Theorems100.Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect

Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean

@@ -168,7 +168,7 @@ theorem card_le_two_pow {x k : ℕ} :
     card M₁ ≤ card (image f K) := card_le_of_subset h
     _ ≤ card K := card_image_le
     _ ≤ 2 ^ card (image Nat.succ (range k)) := by simp only [card_powerset]; rfl
-    _ ≤ 2 ^ card (range k) := (pow_le_pow one_le_two card_image_le)
+    _ ≤ 2 ^ card (range k) := (pow_le_pow_right one_le_two card_image_le)
     _ = 2 ^ k := by rw [card_range k]
 #align theorems_100.card_le_two_pow Theorems100.card_le_two_pow
 

Mathlib/Algebra/GeomSum.lean

@@ -209,9 +209,9 @@ theorem sub_one_dvd_pow_sub_one [Ring α] (x : α) (n : ℕ) :
 
 theorem nat_sub_dvd_pow_sub_pow (x y n : ℕ) : x - y ∣ x ^ n - y ^ n := by
   cases' le_or_lt y x with h h
-  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _
+  · have : y ^ n ≤ x ^ n := Nat.pow_le_pow_left h _
     exact mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
-  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_of_le_left h.le _
+  · have : x ^ n ≤ y ^ n := Nat.pow_le_pow_left h.le _
     exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)
 #align nat_sub_dvd_pow_sub_pow nat_sub_dvd_pow_sub_pow
 

Mathlib/Algebra/GroupPower/CovariantClass.lean

@@ -31,15 +31,15 @@ section Left
 
 variable [CovariantClass M M (· * ·) (· ≤ ·)] {x : M}
 
-@[to_additive (attr := mono) nsmul_le_nsmul_of_le_right]
-theorem pow_le_pow_of_le_left' [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {a b : M} (hab : a ≤ b) :
+@[to_additive (attr := mono) nsmul_le_nsmul_right]
+theorem pow_le_pow_left' [CovariantClass M M (swap (· * ·)) (· ≤ ·)] {a b : M} (hab : a ≤ b) :
     ∀ i : ℕ, a ^ i ≤ b ^ i
   | 0 => by simp
   | k + 1 => by
     rw [pow_succ, pow_succ]
-    exact mul_le_mul' hab (pow_le_pow_of_le_left' hab k)
-#align pow_le_pow_of_le_left' pow_le_pow_of_le_left'
-#align nsmul_le_nsmul_of_le_right nsmul_le_nsmul_of_le_right
+    exact mul_le_mul' hab (pow_le_pow_left' hab k)
+#align pow_le_pow_of_le_left' pow_le_pow_left'
+#align nsmul_le_nsmul_of_le_right nsmul_le_nsmul_right
 
 @[to_additive nsmul_nonneg]
 theorem one_le_pow_of_one_le' {a : M} (H : 1 ≤ a) : ∀ n : ℕ, 1 ≤ a ^ n
@@ -56,20 +56,20 @@ theorem pow_le_one' {a : M} (H : a ≤ 1) (n : ℕ) : a ^ n ≤ 1 :=
 #align pow_le_one' pow_le_one'
 #align nsmul_nonpos nsmul_nonpos
 
-@[to_additive nsmul_le_nsmul]
-theorem pow_le_pow' {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
+@[to_additive nsmul_le_nsmul_left]
+theorem pow_le_pow_right' {a : M} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
   let ⟨k, hk⟩ := Nat.le.dest h
   calc
     a ^ n ≤ a ^ n * a ^ k := le_mul_of_one_le_right' (one_le_pow_of_one_le' ha _)
     _ = a ^ m := by rw [← hk, pow_add]
-#align pow_le_pow' pow_le_pow'
-#align nsmul_le_nsmul nsmul_le_nsmul
+#align pow_le_pow' pow_le_pow_right'
+#align nsmul_le_nsmul nsmul_le_nsmul_left
 
-@[to_additive nsmul_le_nsmul_of_nonpos]
-theorem pow_le_pow_of_le_one' {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
-  @pow_le_pow' Mᵒᵈ _ _ _ _ _ _ ha h
-#align pow_le_pow_of_le_one' pow_le_pow_of_le_one'
-#align nsmul_le_nsmul_of_nonpos nsmul_le_nsmul_of_nonpos
+@[to_additive nsmul_le_nsmul_left_of_nonpos]
+theorem pow_le_pow_right_of_le_one' {a : M} {n m : ℕ} (ha : a ≤ 1) (h : n ≤ m) : a ^ m ≤ a ^ n :=
+  pow_le_pow_right' (M := Mᵒᵈ) ha h
+#align pow_le_pow_of_le_one' pow_le_pow_right_of_le_one'
+#align nsmul_le_nsmul_of_nonpos nsmul_le_nsmul_left_of_nonpos
 
 @[to_additive nsmul_pos]
 theorem one_lt_pow' {a : M} (ha : 1 < a) {k : ℕ} (hk : k ≠ 0) : 1 < a ^ k := by
@@ -88,20 +88,20 @@ theorem pow_lt_one' {a : M} (ha : a < 1) {k : ℕ} (hk : k ≠ 0) : a ^ k < 1 :=
 #align pow_lt_one' pow_lt_one'
 #align nsmul_neg nsmul_neg
 
-@[to_additive nsmul_lt_nsmul]
-theorem pow_lt_pow' [CovariantClass M M (· * ·) (· < ·)] {a : M} {n m : ℕ} (ha : 1 < a)
+@[to_additive nsmul_lt_nsmul_left]
+theorem pow_lt_pow_right' [CovariantClass M M (· * ·) (· < ·)] {a : M} {n m : ℕ} (ha : 1 < a)
     (h : n < m) : a ^ n < a ^ m := by
   rcases Nat.le.dest h with ⟨k, rfl⟩; clear h
   rw [pow_add, pow_succ', mul_assoc, ← pow_succ]
   exact lt_mul_of_one_lt_right' _ (one_lt_pow' ha k.succ_ne_zero)
-#align pow_lt_pow' pow_lt_pow'
-#align nsmul_lt_nsmul nsmul_lt_nsmul
+#align pow_lt_pow_right' pow_lt_pow_right'
+#align nsmul_lt_nsmul_left nsmul_lt_nsmul_left
 
-@[to_additive nsmul_strictMono_right]
-theorem pow_strictMono_left [CovariantClass M M (· * ·) (· < ·)] {a : M} (ha : 1 < a) :
-    StrictMono ((a ^ ·) : ℕ → M) := fun _ _ => pow_lt_pow' ha
-#align pow_strict_mono_left pow_strictMono_left
-#align nsmul_strict_mono_right nsmul_strictMono_right
+@[to_additive nsmul_left_strictMono]
+theorem pow_right_strictMono' [CovariantClass M M (· * ·) (· < ·)] {a : M} (ha : 1 < a) :
+    StrictMono ((a ^ ·) : ℕ → M) := fun _ _ => pow_lt_pow_right' ha
+#align pow_strict_mono_left pow_right_strictMono'
+#align nsmul_strict_mono_right nsmul_left_strictMono
 
 @[to_additive Left.pow_nonneg]
 theorem Left.one_le_pow_of_le (hx : 1 ≤ x) : ∀ {n : ℕ}, 1 ≤ x ^ n
@@ -150,24 +150,22 @@ end Right
 section CovariantLTSwap
 
 variable [Preorder β] [CovariantClass M M (· * ·) (· < ·)]
-  [CovariantClass M M (swap (· * ·)) (· < ·)] {f : β → M}
+  [CovariantClass M M (swap (· * ·)) (· < ·)] {f : β → M} {n : ℕ}
 
-@[to_additive StrictMono.nsmul_left]
-theorem StrictMono.pow_right' (hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a => f a ^ n
+@[to_additive StrictMono.const_nsmul]
+theorem StrictMono.pow_const (hf : StrictMono f) : ∀ {n : ℕ}, n ≠ 0 → StrictMono (f · ^ n)
   | 0, hn => (hn rfl).elim
   | 1, _ => by simpa
   | Nat.succ <| Nat.succ n, _ => by
-    simp_rw [pow_succ _ (n + 1)]
-    exact hf.mul' (StrictMono.pow_right' hf n.succ_ne_zero)
-#align strict_mono.pow_right' StrictMono.pow_right'
-#align strict_mono.nsmul_left StrictMono.nsmul_left
-
-/-- See also `pow_strictMono_right` -/
-@[to_additive nsmul_strictMono_left]  -- Porting note: nolint to_additive_doc
-theorem pow_strictMono_right' {n : ℕ} (hn : n ≠ 0) : StrictMono fun a : M => a ^ n :=
-  strictMono_id.pow_right' hn
-#align pow_strict_mono_right' pow_strictMono_right'
-#align nsmul_strict_mono_left nsmul_strictMono_left
+    simpa only [pow_succ] using hf.mul' (hf.pow_const n.succ_ne_zero)
+#align strict_mono.pow_const StrictMono.pow_const
+#align strict_mono.const_nsmul StrictMono.const_nsmul
+
+/-- See also `pow_left_strictMonoOn`. -/
+@[to_additive nsmul_right_strictMono]  -- Porting note: nolint to_additive_doc
+theorem pow_left_strictMono (hn : n ≠ 0) : StrictMono (· ^ n : M → M) := strictMono_id.pow_const hn
+#align pow_strict_mono_right' pow_left_strictMono
+#align nsmul_strict_mono_left nsmul_right_strictMono
 
 end CovariantLTSwap
 
@@ -176,14 +174,14 @@ section CovariantLESwap
 variable [Preorder β] [CovariantClass M M (· * ·) (· ≤ ·)]
   [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
 
-@[to_additive Monotone.nsmul_left]
+@[to_additive Monotone.const_nsmul]
 theorem Monotone.pow_right {f : β → M} (hf : Monotone f) : ∀ n : ℕ, Monotone fun a => f a ^ n
   | 0 => by simpa using monotone_const
   | n + 1 => by
     simp_rw [pow_succ]
     exact hf.mul' (Monotone.pow_right hf _)
 #align monotone.pow_right Monotone.pow_right
-#align monotone.nsmul_left Monotone.nsmul_left
+#align monotone.const_nsmul Monotone.const_nsmul
 
 @[to_additive nsmul_mono_left]
 theorem pow_mono_right (n : ℕ) : Monotone fun a : M => a ^ n :=
@@ -258,29 +256,29 @@ theorem pow_eq_one_iff {x : M} {n : ℕ} (hn : n ≠ 0) : x ^ n = 1 ↔ x = 1 :=
 
 variable [CovariantClass M M (· * ·) (· < ·)] {a : M} {m n : ℕ}
 
-@[to_additive nsmul_le_nsmul_iff]
-theorem pow_le_pow_iff' (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
-  (pow_strictMono_left ha).le_iff_le
-#align pow_le_pow_iff' pow_le_pow_iff'
-#align nsmul_le_nsmul_iff nsmul_le_nsmul_iff
+@[to_additive nsmul_le_nsmul_iff_left]
+theorem pow_le_pow_iff_right' (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
+  (pow_right_strictMono' ha).le_iff_le
+#align pow_le_pow_iff' pow_le_pow_iff_right'
+#align nsmul_le_nsmul_iff nsmul_le_nsmul_iff_left
 
-@[to_additive nsmul_lt_nsmul_iff]
-theorem pow_lt_pow_iff' (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
-  (pow_strictMono_left ha).lt_iff_lt
-#align pow_lt_pow_iff' pow_lt_pow_iff'
-#align nsmul_lt_nsmul_iff nsmul_lt_nsmul_iff
+@[to_additive nsmul_lt_nsmul_iff_left]
+theorem pow_lt_pow_iff_right' (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
+  (pow_right_strictMono' ha).lt_iff_lt
+#align pow_lt_pow_iff' pow_lt_pow_iff_right'
+#align nsmul_lt_nsmul_iff nsmul_lt_nsmul_iff_left
 
 end CovariantLE
 
 section CovariantLESwap
 
 variable [CovariantClass M M (· * ·) (· ≤ ·)] [CovariantClass M M (swap (· * ·)) (· ≤ ·)]
 
-@[to_additive lt_of_nsmul_lt_nsmul]
-theorem lt_of_pow_lt_pow' {a b : M} (n : ℕ) : a ^ n < b ^ n → a < b :=
+@[to_additive lt_of_nsmul_lt_nsmul_right]
+theorem lt_of_pow_lt_pow_left' {a b : M} (n : ℕ) : a ^ n < b ^ n → a < b :=
   (pow_mono_right _).reflect_lt
-#align lt_of_pow_lt_pow' lt_of_pow_lt_pow'
-#align lt_of_nsmul_lt_nsmul lt_of_nsmul_lt_nsmul
+#align lt_of_pow_lt_pow' lt_of_pow_lt_pow_left'
+#align lt_of_nsmul_lt_nsmul lt_of_nsmul_lt_nsmul_right
 
 @[to_additive min_lt_of_add_lt_two_nsmul]
 theorem min_lt_of_mul_lt_sq {a b c : M} (h : a * b < c ^ 2) : min a b < c := by
@@ -300,11 +298,11 @@ section CovariantLTSwap
 
 variable [CovariantClass M M (· * ·) (· < ·)] [CovariantClass M M (swap (· * ·)) (· < ·)]
 
-@[to_additive le_of_nsmul_le_nsmul]
-theorem le_of_pow_le_pow' {a b : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b :=
-  (pow_strictMono_right' hn).le_iff_le.1
-#align le_of_pow_le_pow' le_of_pow_le_pow'
-#align le_of_nsmul_le_nsmul le_of_nsmul_le_nsmul
+@[to_additive le_of_nsmul_le_nsmul_right']
+theorem le_of_pow_le_pow_left' {a b : M} {n : ℕ} (hn : n ≠ 0) : a ^ n ≤ b ^ n → a ≤ b :=
+  (pow_left_strictMono hn).le_iff_le.1
+#align le_of_pow_le_pow' le_of_pow_le_pow_left'
+#align le_of_nsmul_le_nsmul le_of_nsmul_le_nsmul_right'
 
 @[to_additive min_le_of_add_le_two_nsmul]
 theorem min_le_of_mul_le_sq {a b c : M} (h : a * b ≤ c ^ 2) : min a b ≤ c := by

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -326,12 +326,12 @@ theorem one_lt_zpow' (ha : 1 < a) {k : ℤ} (hk : (0 : ℤ) < k) : 1 < a ^ k :=
 #align zsmul_pos zsmul_pos
 
 @[to_additive zsmul_strictMono_left]
-theorem zpow_strictMono_right (ha : 1 < a) : StrictMono fun n : ℤ => a ^ n := fun m n h =>
+theorem zpow_right_strictMono (ha : 1 < a) : StrictMono fun n : ℤ => a ^ n := fun m n h =>
   calc
     a ^ m = a ^ m * 1 := (mul_one _).symm
     _ < a ^ m * a ^ (n - m) := mul_lt_mul_left' (one_lt_zpow' ha <| sub_pos_of_lt h) _
     _ = a ^ n := by rw [← zpow_add]; simp
-#align zpow_strict_mono_right zpow_strictMono_right
+#align zpow_strict_mono_right zpow_right_strictMono
 #align zsmul_strict_mono_left zsmul_strictMono_left
 
 @[to_additive zsmul_mono_left]
@@ -351,19 +351,19 @@ theorem zpow_le_zpow (ha : 1 ≤ a) (h : m ≤ n) : a ^ m ≤ a ^ n :=
 
 @[to_additive]
 theorem zpow_lt_zpow (ha : 1 < a) (h : m < n) : a ^ m < a ^ n :=
-  zpow_strictMono_right ha h
+  zpow_right_strictMono ha h
 #align zpow_lt_zpow zpow_lt_zpow
 #align zsmul_lt_zsmul zsmul_lt_zsmul
 
 @[to_additive]
 theorem zpow_le_zpow_iff (ha : 1 < a) : a ^ m ≤ a ^ n ↔ m ≤ n :=
-  (zpow_strictMono_right ha).le_iff_le
+  (zpow_right_strictMono ha).le_iff_le
 #align zpow_le_zpow_iff zpow_le_zpow_iff
 #align zsmul_le_zsmul_iff zsmul_le_zsmul_iff
 
 @[to_additive]
 theorem zpow_lt_zpow_iff (ha : 1 < a) : a ^ m < a ^ n ↔ m < n :=
-  (zpow_strictMono_right ha).lt_iff_lt
+  (zpow_right_strictMono ha).lt_iff_lt
 #align zpow_lt_zpow_iff zpow_lt_zpow_iff
 #align zsmul_lt_zsmul_iff zsmul_lt_zsmul_iff
 
@@ -746,9 +746,9 @@ theorem strictMono_pow_bit1 (n : ℕ) : StrictMono fun a : R => a ^ bit1 n := by
   cases' le_total a 0 with ha ha
   · cases' le_or_lt b 0 with hb hb
     · rw [← neg_lt_neg_iff, ← neg_pow_bit1, ← neg_pow_bit1]
-      exact pow_lt_pow_of_lt_left (neg_lt_neg hab) (neg_nonneg.2 hb) (bit1_pos (zero_le n))
+      exact pow_lt_pow_left (neg_lt_neg hab) (neg_nonneg.2 hb) n.bit1_ne_zero
     · exact (pow_bit1_nonpos_iff.2 ha).trans_lt (pow_bit1_pos_iff.2 hb)
-  · exact pow_lt_pow_of_lt_left hab ha (bit1_pos (zero_le n))
+  · exact pow_lt_pow_left hab ha n.bit1_ne_zero
 #align strict_mono_pow_bit1 strictMono_pow_bit1
 
 end bit1