α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
have h : ∃ n : ℕ, x < y ^ n := pow_unbounded_of_one_lt _ hy
no goals
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
classical exact
    let n := Nat.find h
    have hn : x < y ^ n := Nat.find_spec h
    have hnp : 0 < n :=
      pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
    have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
    have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
    ⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩
no goals
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
exact
let n := Nat.find h
have hn : x < y ^ n := Nat.find_spec h
have hnp : 0 < n :=
pos_iff_ne_zero.2 fun hn0 => by rw [hn0, pow_zero] at hn; exact not_le_of_gt hn hx
have hnsp : Nat.pred n + 1 = n := Nat.succ_pred_eq_of_pos hnp
have hltn : Nat.pred n < n := Nat.pred_lt (ne_of_gt hnp)
⟨Nat.pred n, le_of_not_lt (Nat.find_min h hltn), by rwa [hnsp]⟩
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hn0 : n = 0
⊢ False
rw [hn0, pow_zero] at hn
no goals
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < 1
hn0 : n = 0
⊢ False
exact not_le_of_gt hn hx
no goals
α : Type u_1
inst✝¹ : LinearOrderedRing α
inst✝ : Archimedean α
x y : α
hx : 1 ≤ x
hy : 1 < y
h : ∃ n, x < y ^ n
n : ℕ := Nat.find h
hn : x < y ^ n
hnp : 0 < n
hnsp : Nat.pred n + 1 = n
hltn : Nat.pred n < n
⊢ x < y ^ (Nat.pred n + 1)
rwa [hnsp]