z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
have hn' : 0 < (n : ℝ) := by exact_mod_cast hn.bot_lt
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
obtain ⟨q, hxq, hqy⟩ :=
  exists_rat_btwn (rpow_lt_rpow (le_max_left 0 x) (max_lt hy h) <| inv_pos.mpr hn')
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
have := rpow_nonneg_of_nonneg (le_max_left 0 x) n⁻¹
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
have hq := this.trans_lt hxq
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hxq : max 0 x ^ (↑n)⁻¹ < ↑q
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
replace hxq := rpow_lt_rpow this hxq hn'
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n
hqy : ↑q ^ ↑n < (y ^ (↑n)⁻¹) ^ ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
hqy : ↑q < y ^ (↑n)⁻¹
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
replace hqy := rpow_lt_rpow hq.le hqy hn'
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y

z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n
⊢ 0 ≤ y

z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ n < ↑q ^ n
hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n
⊢ 0 ≤ max 0 x
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n
hqy : ↑q ^ ↑n < (y ^ (↑n)⁻¹) ^ ↑n
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
rw [rpow_nat_cast, rpow_nat_cast, rpow_nat_inv_pow_nat _ hn] at hxq hqy
no goals
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
⊢ 0 < ↑n
exact_mod_cast hn.bot_lt
no goals
case intro.intro
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < y
⊢ ∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
exact ⟨q, by exact_mod_cast hq, (le_max_right _ _).trans_lt hxq, hqy⟩
no goals
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < y
⊢ 0 < q
exact_mod_cast hq
no goals
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : max 0 x < ↑q ^ n
hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n
⊢ 0 ≤ y
exact hy.le
no goals
z x✝ y✝ : ℝ
n : ℕ
hn : n ≠ 0
x y : ℝ
h : x < y
hy : 0 < y
hn' : 0 < ↑n
q : ℚ
this : 0 ≤ max 0 x ^ (↑n)⁻¹
hq : 0 < ↑q
hxq : (max 0 x ^ (↑n)⁻¹) ^ n < ↑q ^ n
hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n
⊢ 0 ≤ max 0 x
exact le_max_left _ _