case intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (y ^ n) (y ^ (n + 1))
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q : ℝ≥0
x y : ℝ≥0∞
hx : x ≠ 0
h'x : x ≠ ⊤
hy : 1 < y
h'y : y ≠ ⊤
⊢ ∃ n, x ∈ Ioc (y ^ n) (y ^ (n + 1))
lift x to ℝ≥0 using h'x
case intro.intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
case intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q : ℝ≥0
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ⊤
x : ℝ≥0
hx : ↑x ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (y ^ n) (y ^ (n + 1))
lift y to ℝ≥0 using h'y
case intro.intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
case intro.intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
have A : y ≠ 0 := by simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
case intro.intro.intro.intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
case intro.intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) := by
  refine' NNReal.exists_mem_Ioc_zpow _ (one_lt_coe_iff.1 hy)
  simpa only [Ne.def, coe_eq_zero] using hx
case intro.intro.intro.intro.refine'_1
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x

case intro.intro.intro.intro.refine'_2
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)
case intro.intro.intro.intro
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ioc (↑y ^ n) (↑y ^ (n + 1))
refine' ⟨n, _, _⟩
no goals
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
⊢ y ≠ 0
simpa only [Ne.def, coe_eq_zero] using (zero_lt_one.trans hy).ne'
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n < x ∧ x ≤ y ^ (n + 1)
refine' NNReal.exists_mem_Ioc_zpow _ (one_lt_coe_iff.1 hy)
no goals
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ x ≠ 0
simpa only [Ne.def, coe_eq_zero] using hx
no goals
case intro.intro.intro.intro.refine'_1
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑y ^ n < ↑x
rwa [← ENNReal.coe_zpow A, ENNReal.coe_lt_coe]
no goals
case intro.intro.intro.intro.refine'_2
α : Type ?u.560921
β : Type ?u.560924
a b c d : ℝ≥0∞
r p q x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n < x
h'n : x ≤ y ^ (n + 1)
⊢ ↑x ≤ ↑y ^ (n + 1)
rwa [← ENNReal.coe_zpow A, ENNReal.coe_le_coe]