feat: if 1 < x then y ^ n < x for some 1 < y (#28942)

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Author Name <yael.dillies@gmail.com>

Author: vihdzp

Mathlib/Algebra/Order/Group/DenselyOrdered.lean

@@ -3,9 +3,12 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
+import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.Unbundled.Basic
-import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
+import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
+import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
+import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 
 /-!
 # Lemmas about densely linearly ordered groups.
@@ -83,3 +86,42 @@ lemma mul_le_of_forall_lt [CommGroup α] [LinearOrder α] [MulLeftMono α]
   exact hd.le.trans (h a' ha' b' hb')
 
 end DenselyOrdered
+
+variable {M : Type*} [LinearOrder M] [DenselyOrdered M] {x : M}
+
+section Monoid
+variable [CommMonoid M] [ExistsMulOfLE M] [IsOrderedCancelMonoid M]
+
+@[to_additive]
+private theorem exists_pow_two_le_of_one_lt (hx : 1 < x) : ∃ y : M, 1 < y ∧ y ^ 2 ≤ x := by
+  obtain ⟨y, hy, hyx⟩ := exists_between hx
+  obtain hyx | hxy := le_total (y ^ 2) x
+  · exact ⟨y, hy, hyx⟩
+  obtain ⟨z, hz, rfl⟩ := exists_one_lt_mul_of_lt' hyx
+  exact ⟨z, hz, by simpa [pow_succ] using hxy⟩
+
+@[to_additive]
+theorem exists_pow_lt_of_one_lt (hx : 1 < x) : ∀ n : ℕ, ∃ y : M, 1 < y ∧ y ^ n < x
+  | 0 => ⟨x, by simpa⟩
+  | 1 => by simpa using exists_between hx
+  | n + 2 => by
+    obtain ⟨y, hy, hyx⟩ := exists_pow_lt_of_one_lt hx (n + 1)
+    obtain ⟨z, hz, hzy⟩ := exists_pow_two_le_of_one_lt hy
+    refine ⟨z, hz, hyx.trans_le' ?_⟩
+    calc z ^ (n + 2)
+      _ ≤ z ^ (2 * (n + 1)) := pow_right_monotone hz.le (by omega)
+      _ = (z ^ 2) ^ (n + 1) := by rw [pow_mul]
+      _ ≤ y ^ (n + 1) := pow_le_pow_left' hzy (n + 1)
+
+end Monoid
+
+section Group
+variable [CommGroup M] [IsOrderedCancelMonoid M]
+
+@[to_additive]
+theorem exists_lt_pow_of_lt_one (hx : x < 1) (n : ℕ) : ∃ y : M, y < 1 ∧ x < y ^ n := by
+  obtain ⟨y, hy, hy'⟩ := exists_pow_lt_of_one_lt (one_lt_inv_of_inv hx) n
+  use y⁻¹, inv_lt_one_of_one_lt hy
+  simpa [lt_inv'] using hy'
+
+end Group