-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_pow_btwn {n : ℕ} (hn : n ≠ 0) {x y : α} (h : x < y) (hy : 0 < y) :
    ∃ q : α, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Proof state:
case refine_1
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ y / δ ≤ ↑m

Tactic:
exact (lt_add_of_pos_right _ <| by positivity).le.trans hm

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
let m := Nat.find ex

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ 0 ≤ y / δ

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : α := ↑m.pred * δ
qny : q ^ n < y
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have q1y : |q| < max 1 y := (abs_eq_self.mpr <| by positivity).trans_lt <| lt_max_iff.mpr
  (or_iff_not_imp_left.mpr fun q1 ↦ (le_self_pow₀ (le_of_not_lt q1) hn).trans_lt qny)

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : α := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < 1 ⊔ y
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : α := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < 1 ⊔ y
xqn : x ⊔ 0 < q ^ n
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
exact ⟨q, lt_of_le_of_ne (by positivity) fun q0 ↦
  (le_sup_right.trans_lt xqn).ne <| q0 ▸ (zero_pow hn).symm, le_sup_left.trans_lt xqn, qny⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : α := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < 1 ⊔ y
⊢ (↑m * δ) ^ n - (y - x ⊔ 0) < (↑m * δ) ^ n - ((↑m * δ) ^ n - q ^ n)

Tactic:
refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _

Result:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : α := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < 1 ⊔ y
⊢ |↑m * δ - q| ≤ δ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : α := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < 1 ⊔ y
⊢ 0 ≤ δ

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
δ : α
δ_pos : δ > 0
cont : ∀ (q r : α), |r| ≤ 1 ⊔ y → |q - r| ≤ δ → |q ^ n - r ^ n| < y - x ⊔ 0
ex : ∃ m, y ≤ (↑m * δ) ^ n
m : ℕ := Nat.find ex
m_pos : 0 < m
q : α := ↑m.pred * δ
qny : q ^ n < y
q1y : |q| < 1 ⊔ y
⊢ x ⊔ 0 = y - (y - x ⊔ 0)

Tactic:
rw [sub_sub_cancel]

Result:
no goals