case intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
obtain ⟨q₂, hx₂, hy₂⟩ := exists_rat_btwn (max_lt h hy)
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
obtain ⟨q₁, hx₁, hq₁₂⟩ := exists_rat_btwn hx₂
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
this : 0 < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
have : (0 : α) < q₂ := (le_max_right _ _).trans_lt hx₂
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : ↑q₁ < ↑q₂
this : 0 < ↑q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
norm_cast  at hq₁₂ this
case intro.intro.intro.intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max 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
case intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max x 0 < ↑q₁
hq₁₂ : q₁ < q₂
this : 0 < q₂
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
obtain ⟨q, hq, hq₁, hq₂⟩ := exists_rat_pow_btwn_rat hn hq₁₂ this
no goals
case intro.intro.intro.intro.intro.intro.intro
z x✝ y✝ : ℝ
n : ℕ
α : Type u_1
inst✝¹ : LinearOrderedField α
inst✝ : Archimedean α
hn : n ≠ 0
x y : α
h : x < y
hy : 0 < y
q₂ : ℚ
hx₂ : max x 0 < ↑q₂
hy₂ : ↑q₂ < y
q₁ : ℚ
hx₁ : max 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
refine' ⟨q, hq, (le_max_left _ _).trans_lt <| hx₁.trans _, hy₂.trans' _⟩ <;> assumption_mod_cast