-- 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:
α : 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
⊢ ¬y ≤ (↑0 * δ) ^ n

Tactic:
simpa [zero_pow hn] using hy

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have ⟨δ, δ_pos, cont⟩ := uniform_continuous_npow_on_bounded (max 1 y)
  (sub_pos.mpr <| max_lt_iff.mpr ⟨h, hy⟩) n

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
⊢ ∃ 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
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have xqn : max x 0 < q ^ n :=
  calc _ = y - (y - max x 0) := by rw [sub_sub_cancel]
    _ ≤ (m * δ) ^ n - (y - max x 0) := sub_le_sub_right (Nat.find_spec ex) _
    _ < (m * δ) ^ n - ((m * δ) ^ n - q ^ n) := by
      refine sub_lt_sub_left ((le_abs_self _).trans_lt <| cont _ _ q1y.le ?_) _
      rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
        add_sub_cancel_left, one_mul, abs_eq_self.mpr (by positivity)]
    _ = q ^ n := sub_sub_cancel ..

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
xqn : x ⊔ 0 < q ^ n
⊢ ∃ 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
⊢ 0 ≤ q

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
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ ∃ m, y ≤ (↑m * δ) ^ n

Tactic:
refine ⟨m, le_trans ?_ (le_self_pow₀ ?_ hn)⟩ <;> rw [← div_le_iff₀ δ_pos]

Result:
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

case refine_2
α : 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
⊢ 1 / δ ≤ ↑m

Proof state:
case refine_2
α : 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
⊢ 1 / δ ≤ ↑m

Tactic:
exact (le_add_of_nonneg_left <| by positivity).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
⊢ ∃ m, y ≤ (↑m * δ) ^ n

Tactic:
have ⟨m, hm⟩ := exists_nat_ge (y / δ + 1 / δ)

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
m : ℕ
hm : y / δ + 1 / δ ≤ ↑m
⊢ ∃ m, y ≤ (↑m * δ) ^ n

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
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have m_pos : 0 < m := (Nat.find_pos _).mpr <| by simpa [zero_pow hn] using hy

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, 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 * δ
⊢ ∃ q, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
have qny : q ^ n < y := lt_of_not_le (Nat.find_min ex <| Nat.pred_lt m_pos.ne')

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
⊢ ∃ 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
⊢ |↑m * δ - q| ≤ δ

Tactic:
rw [← Nat.succ_pred_eq_of_pos m_pos, Nat.cast_succ, ← sub_mul,
  add_sub_cancel_left, one_mul, abs_eq_self.mpr (by 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, 0 < q ∧ x < q ^ n ∧ q ^ n < y

Tactic:
let q := m.pred * δ

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 * δ
⊢ ∃ 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 < 1 / δ

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
⊢ 0 ≤ q

Tactic:
positivity

Result:
no goals