x : ℝ
hx : Liouville x
p : ℝ
this : LiouvilleWith (↑⌈p⌉₊) x
⊢ LiouvilleWith p x

case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith p x
suffices : LiouvilleWith ⌈p⌉₊ x
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x
x : ℝ
hx : Liouville x
p : ℝ
this : LiouvilleWith (↑⌈p⌉₊) x
⊢ LiouvilleWith p x

case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x
exact this.mono (Nat.le_ceil p)
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ abs (x - ↑a / ↑x_1) < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < 1 / ↑x_1 ^ ↑⌈p⌉₊
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊) x
refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ abs (x - ↑m / ↑b) < 1 / ↑b ^ ↑⌈p⌉₊
case this
x : ℝ
hx : Liouville x
p : ℝ
⊢ ∀ (x_1 : ℕ),
    (1 < x_1 ∧ ∃ a, x ≠ ↑a / ↑x_1 ∧ abs (x - ↑a / ↑x_1) < 1 / ↑x_1 ^ ⌈p⌉₊) →
      ∃ m, x ≠ ↑m / ↑x_1 ∧ abs (x - ↑m / ↑x_1) < 1 / ↑x_1 ^ ↑⌈p⌉₊
rintro b ⟨_hb, a, hne, hlt⟩
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ ⌈p⌉₊
⊢ abs (x - ↑a / ↑b) < 1 / ↑b ^ ↑⌈p⌉₊
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ ⌈p⌉₊
⊢ ∃ m, x ≠ ↑m / ↑b ∧ abs (x - ↑m / ↑b) < 1 / ↑b ^ ↑⌈p⌉₊
refine ⟨a, hne, ?_⟩
no goals
case this.intro.intro.intro
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ ⌈p⌉₊
⊢ abs (x - ↑a / ↑b) < 1 / ↑b ^ ↑⌈p⌉₊
rwa [rpow_nat_cast]