-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem exists_rat_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
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
obtain ⟨q₂, hx₂, hy₂⟩ := exists_rat_btwn (max_lt h hy)

Result:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Proof state:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
refine ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans ?_, hy₂.trans' ?_⟩ <;> assumption_mod_cast

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
obtain ⟨q, hq, hq₁, hq₂⟩ := exists_pow_btwn hn hq₁₂ this

Result:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
q : ℚ
hq : 0 < q
hq₁ : q₁ < q ^ n
hq₂ : q ^ n < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
obtain ⟨q₁, hx₁, hq₁₂⟩ := exists_rat_btwn hx₂

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
this : 0 < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
norm_cast at hq₁₂ this

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

Tactic:
have : (0 : α) < q₂ := (le_max_right _ _).trans_lt hx₂

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
n : ℕ
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : x ⊔ 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : x ⊔ 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
this : 0 < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y