chore: generalise pow monotonicity lemmas to groups with zero (#18967)

In particular they now apply to `ℤₘ₀`

From FLT

Author: YaelDillies

Archive/Imo/Imo2001Q2.lean

@@ -39,7 +39,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_left two_ne_zero (by positivity)
+  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

@@ -64,7 +64,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_left two_ne_zero (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

@@ -60,10 +60,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_left 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_left 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

@@ -27,7 +27,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 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]
 
 end Imo2008Q4
 

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -103,7 +103,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_right (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 k.succ_pos)
     contrapose! hm
     simp [hm]
 

Mathlib/Algebra/Order/CompleteField.lean

@@ -237,7 +237,7 @@ theorem le_inducedMap_mul_self_of_mem_cutMap (ha : 0 < a) (b : β) (hb : b ∈ c
   · rw [pow_two] at hqa ⊢
     exact mul_self_le_mul_self (mod_cast hq'.le)
       (le_csSup (cutMap_bddAbove β a) <|
-        coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self ha.le hqa)
+        coe_mem_cutMap_iff.2 <| lt_of_mul_self_lt_mul_self₀ ha.le hqa)
 
 /-- Preparatory lemma for `inducedOrderRingHom`. -/
 theorem exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self (ha : 0 < a) (b : β)
@@ -251,7 +251,7 @@ theorem exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self (ha : 0 < a) (b : 
   refine ⟨(q ^ 2 : ℚ), coe_mem_cutMap_iff.2 ?_, hbq⟩
   rw [pow_two] at hqa ⊢
   push_cast
-  obtain ⟨q', hq', hqa'⟩ := lt_inducedMap_iff.1 (lt_of_mul_self_lt_mul_self
+  obtain ⟨q', hq', hqa'⟩ := lt_inducedMap_iff.1 (lt_of_mul_self_lt_mul_self₀
     (inducedMap_nonneg ha.le) hqa)
   exact mul_self_lt_mul_self (mod_cast hq.le) (hqa'.trans' <| by assumption_mod_cast)
 

Mathlib/Algebra/Order/Field/Basic.lean

@@ -411,7 +411,7 @@ theorem one_div_pow_le_one_div_pow_of_le (a1 : 1 ≤ a) {m n : ℕ} (mn : m ≤
 
 theorem one_div_pow_lt_one_div_pow_of_lt (a1 : 1 < a) {m n : ℕ} (mn : m < n) :
     1 / a ^ n < 1 / a ^ m := by
-  refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right a1 mn) <;>
+  refine (one_div_lt_one_div ?_ ?_).2 (pow_lt_pow_right₀ a1 mn) <;>
     exact pow_pos (zero_lt_one.trans a1) _
 
 theorem one_div_pow_anti (a1 : 1 ≤ a) : Antitone fun n : ℕ => 1 / a ^ n := fun _ _ =>

Mathlib/Algebra/Order/Group/Nat.lean

@@ -47,7 +47,7 @@ instance instOrderedSub : OrderedSub ℕ := by
 
 variable {α : Type*} {n : ℕ} {f : α → ℕ}
 
-/-- See also `pow_left_strictMonoOn`. -/
+/-- See also `pow_left_strictMonoOn₀`. -/
 protected lemma pow_left_strictMono (hn : n ≠ 0) : StrictMono (· ^ n : ℕ → ℕ) :=
   fun _ _ h ↦ Nat.pow_lt_pow_left h hn
 

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -235,9 +235,6 @@ lemma pow_lt_pow_succ (ha : 1 < a) : a ^ n < a ^ n.succ := by
   rw [← one_mul (a ^ n), pow_succ']
   exact mul_lt_mul_of_pos_right ha (pow_pos (zero_lt_one.trans ha) _)
 
-lemma pow_lt_pow_right₀ (ha : 1 < a) (hmn : m < n) : a ^ m < a ^ n := by
-  induction' hmn with n _ ih; exacts [pow_lt_pow_succ ha, lt_trans ih (pow_lt_pow_succ ha)]
-
 end LinearOrderedCommGroupWithZero
 
 instance instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

@@ -9,6 +9,7 @@ import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
 import Mathlib.Algebra.Order.ZeroLEOne
 import Mathlib.Tactic.Bound.Attribute
 import Mathlib.Tactic.GCongr.CoreAttrs
+import Mathlib.Tactic.Monotonicity.Attr
 import Mathlib.Tactic.Nontriviality
 
 /-!
@@ -1008,12 +1009,30 @@ lemma pow_right_mono₀ (h : 1 ≤ a) : Monotone (a ^ ·) :=
   monotone_nat_of_le_succ fun n => by
     rw [pow_succ']; exact le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h
 
+/-- `bound` lemma for branching on `1 ≤ a ∨ a ≤ 1` when proving `a ^ n ≤ a ^ m` -/
+@[bound]
+lemma Bound.pow_le_pow_right_of_le_one_or_one_le (h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n) :
+    a ^ n ≤ a ^ m := by
+  obtain ⟨a1, nm⟩ | ⟨a0, a1, mn⟩ := h
+  · exact pow_right_mono₀ a1 nm
+  · exact pow_le_pow_of_le_one a0 a1 mn
+
 @[gcongr]
 lemma pow_le_pow_right₀ (ha : 1 ≤ a) (hmn : m ≤ n) : a ^ m ≤ a ^ n := pow_right_mono₀ ha hmn
 
 lemma le_self_pow₀ (ha : 1 ≤ a) (hn : n ≠ 0) : a ≤ a ^ n := by
   simpa only [pow_one] using pow_le_pow_right₀ ha <| Nat.pos_iff_ne_zero.2 hn
 
+/-- The `bound` tactic can't handle `m ≠ 0` goals yet, so we express as `0 < m` -/
+@[bound]
+lemma Bound.le_self_pow_of_pos (ha : 1 ≤ a) (hn : 0 < n) : a ≤ a ^ n := le_self_pow₀ ha hn.ne'
+
+@[mono, gcongr, bound]
+theorem pow_le_pow_left₀ (ha : 0 ≤ a) (hab : a ≤ b) : ∀ n, a ^ n ≤ b ^ n
+  | 0 => by simp
+  | n + 1 => by simpa only [pow_succ']
+      using mul_le_mul hab (pow_le_pow_left₀ ha hab _) (pow_nonneg ha _) (ha.trans hab)
+
 end
 
 variable [Preorder α] {f g : α → M₀}
@@ -1044,11 +1063,7 @@ end Preorder
 
 
 section PartialOrder
-variable [PartialOrder M₀] {a b c d : M₀}
-
-@[simp] lemma pow_pos [ZeroLEOneClass M₀] [PosMulStrictMono M₀] (ha : 0 < a) : ∀ n, 0 < a ^ n
-  | 0 => by nontriviality; rw [pow_zero]; exact zero_lt_one
-  | _ + 1 => pow_succ a _ ▸ mul_pos (pow_pos ha _) ha
+variable [PartialOrder M₀] {a b c d : M₀} {m n : ℕ}
 
 lemma mul_self_lt_mul_self [PosMulStrictMono M₀] [MulPosMono M₀] (ha : 0 ≤ a) (hab : a < b) :
     a * a < b * b := mul_lt_mul' hab.le hab ha <| ha.trans_lt hab
@@ -1076,6 +1091,61 @@ lemma lt_mul_right [PosMulStrictMono M₀] (ha : 0 < a) (hb : 1 < b) : a < a * b
 lemma lt_mul_self [ZeroLEOneClass M₀] [MulPosStrictMono M₀] (ha : 1 < a) : a < a * a :=
   lt_mul_left (ha.trans_le' zero_le_one) ha
 
+section strict_mono
+variable [ZeroLEOneClass M₀] [PosMulStrictMono M₀]
+
+@[simp] lemma pow_pos (ha : 0 < a) : ∀ n, 0 < a ^ n
+  | 0 => by nontriviality; rw [pow_zero]; exact zero_lt_one
+  | _ + 1 => pow_succ a _ ▸ mul_pos (pow_pos ha _) ha
+
+lemma sq_pos_of_pos (ha : 0 < a) : 0 < a ^ 2 := pow_pos ha _
+
+variable [MulPosStrictMono M₀]
+
+@[gcongr, bound]
+lemma pow_lt_pow_left₀ (hab : a < b)
+    (ha : 0 ≤ a) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
+  | n + 1, _ => by
+    simpa only [pow_succ] using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
+      (pow_le_pow_left₀ ha hab.le _) hab ha (pow_pos (ha.trans_lt hab) _)
+
+/-- See also `pow_left_strictMono₀` and `Nat.pow_left_strictMono`. -/
+lemma pow_left_strictMonoOn₀ (hn : n ≠ 0) : StrictMonoOn (· ^ n : M₀ → M₀) {a | 0 ≤ a} :=
+  fun _a ha _b _ hab ↦ pow_lt_pow_left₀ hab ha hn
+
+/-- See also `pow_right_strictMono'`. -/
+lemma pow_right_strictMono₀ (h : 1 < a) : StrictMono (a ^ ·) :=
+  have : 0 < a := zero_le_one.trans_lt h
+  strictMono_nat_of_lt_succ fun n => by
+    simpa only [one_mul, pow_succ'] using mul_lt_mul h (le_refl (a ^ n)) (pow_pos this _) this.le
+
+@[gcongr]
+lemma pow_lt_pow_right₀ (h : 1 < a) (hmn : m < n) : a ^ m < a ^ n := pow_right_strictMono₀ h hmn
+
+lemma pow_lt_pow_iff_right₀ (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
+  (pow_right_strictMono₀ h).lt_iff_lt
+
+lemma pow_le_pow_iff_right₀ (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m :=
+  (pow_right_strictMono₀ h).le_iff_le
+
+lemma lt_self_pow₀ (h : 1 < a) (hm : 1 < m) : a < a ^ m := by
+  simpa only [pow_one] using pow_lt_pow_right₀ h hm
+
+lemma pow_right_strictAnti₀ (h₀ : 0 < a) (h₁ : a < 1) : StrictAnti (a ^ ·) :=
+  strictAnti_nat_of_succ_lt fun n => by
+    simpa only [pow_succ', one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one
+
+lemma pow_lt_pow_iff_right_of_lt_one₀ (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m :=
+  (pow_right_strictAnti₀ h₀ h₁).lt_iff_lt
+
+lemma pow_lt_pow_right_of_lt_one₀ (h₀ : 0 < a) (h₁ : a < 1) (hmn : m < n) : a ^ n < a ^ m :=
+  (pow_lt_pow_iff_right_of_lt_one₀ h₀ h₁).2 hmn
+
+lemma pow_lt_self_of_lt_one₀ (h₀ : 0 < a) (h₁ : a < 1) (hn : 1 < n) : a ^ n < a := by
+  simpa only [pow_one] using pow_lt_pow_right_of_lt_one₀ h₀ h₁ hn
+
+end strict_mono
+
 variable [Preorder α] {f g : α → M₀}
 
 lemma strictMono_mul_left_of_pos [PosMulStrictMono M₀] (ha : 0 < a) :
@@ -1108,7 +1178,72 @@ lemma StrictMono.mul [PosMulStrictMono M₀] [MulPosStrictMono M₀] (hf : Stric
     (hg : StrictMono g) (hf₀ : ∀ x, 0 ≤ f x) (hg₀ : ∀ x, 0 ≤ g x) :
     StrictMono (f * g) := fun _ _ h ↦ mul_lt_mul'' (hf h) (hg h) (hf₀ _) (hg₀ _)
 
-end MonoidWithZero.PartialOrder
+end PartialOrder
+
+section LinearOrder
+variable [LinearOrder M₀] [ZeroLEOneClass M₀] [PosMulStrictMono M₀] [MulPosStrictMono M₀] {a b : M₀}
+  {m n : ℕ}
+
+lemma pow_le_pow_iff_left₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b :=
+  (pow_left_strictMonoOn₀ hn).le_iff_le ha hb
+
+lemma pow_lt_pow_iff_left₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b :=
+  (pow_left_strictMonoOn₀ hn).lt_iff_lt ha hb
+
+@[simp]
+lemma pow_left_inj₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : n ≠ 0) : a ^ n = b ^ n ↔ a = b :=
+  (pow_left_strictMonoOn₀ hn).eq_iff_eq ha hb
+
+lemma pow_right_injective₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : Injective (a ^ ·) := by
+  obtain ha₁ | ha₁ := ha₁.lt_or_lt
+  · exact (pow_right_strictAnti₀ ha₀ ha₁).injective
+  · exact (pow_right_strictMono₀ ha₁).injective
+
+@[simp]
+lemma pow_right_inj₀ (ha₀ : 0 < a) (ha₁ : a ≠ 1) : a ^ m = a ^ n ↔ m = n :=
+  (pow_right_injective₀ ha₀ ha₁).eq_iff
+
+lemma pow_le_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1 := by
+  simpa only [one_pow] using pow_le_pow_iff_left₀ ha zero_le_one hn
+
+lemma one_le_pow_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : 1 ≤ a ^ n ↔ 1 ≤ a := by
+  simpa only [one_pow] using pow_le_pow_iff_left₀ zero_le_one ha hn
+
+lemma pow_lt_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n < 1 ↔ a < 1 :=
+  lt_iff_lt_of_le_iff_le (one_le_pow_iff_of_nonneg ha hn)
+
+lemma one_lt_pow_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : 1 < a ^ n ↔ 1 < a := by
+  simpa only [one_pow] using pow_lt_pow_iff_left₀ zero_le_one ha hn
+
+lemma pow_eq_one_iff_of_nonneg (ha : 0 ≤ a) (hn : n ≠ 0) : a ^ n = 1 ↔ a = 1 := by
+  simpa only [one_pow] using pow_left_inj₀ ha zero_le_one hn
+
+lemma sq_le_one_iff₀ (ha : 0 ≤ a) : a ^ 2 ≤ 1 ↔ a ≤ 1 :=
+  pow_le_one_iff_of_nonneg ha (Nat.succ_ne_zero _)
+
+lemma sq_lt_one_iff₀ (ha : 0 ≤ a) : a ^ 2 < 1 ↔ a < 1 :=
+  pow_lt_one_iff_of_nonneg ha (Nat.succ_ne_zero _)
+
+lemma one_le_sq_iff₀ (ha : 0 ≤ a) : 1 ≤ a ^ 2 ↔ 1 ≤ a :=
+  one_le_pow_iff_of_nonneg ha (Nat.succ_ne_zero _)
+
+lemma one_lt_sq_iff₀ (ha : 0 ≤ a) : 1 < a ^ 2 ↔ 1 < a :=
+  one_lt_pow_iff_of_nonneg ha (Nat.succ_ne_zero _)
+
+lemma lt_of_pow_lt_pow_left₀ (n : ℕ) (hb : 0 ≤ b) (h : a ^ n < b ^ n) : a < b :=
+  lt_of_not_ge fun hn => not_lt_of_ge (pow_le_pow_left₀ hb hn _) h
+
+lemma le_of_pow_le_pow_left₀ (hn : n ≠ 0) (hb : 0 ≤ b) (h : a ^ n ≤ b ^ n) : a ≤ b :=
+  le_of_not_lt fun h1 => not_le_of_lt (pow_lt_pow_left₀ h1 hb hn) h
+
+@[simp]
+lemma sq_eq_sq₀ (ha : 0 ≤ a) (hb : 0 ≤ b) : a ^ 2 = b ^ 2 ↔ a = b := pow_left_inj₀ ha hb (by decide)
+
+lemma lt_of_mul_self_lt_mul_self₀ (hb : 0 ≤ b) : a * a < b * b → a < b := by
+  simp_rw [← sq]
+  exact lt_of_pow_lt_pow_left₀ _ hb
+
+end MonoidWithZero.LinearOrder
 
 section CancelMonoidWithZero
 
@@ -1654,4 +1789,4 @@ lemma div_lt_comm₀ (hb : 0 < b) (hc : 0 < c) : a / b < c ↔ a / c < b := by
 end PosMulStrictMono
 end CommGroupWithZero
 
-set_option linter.style.longFile 1700
+set_option linter.style.longFile 1900