x : ℝ
hx : Liouville x
n : ℕ
H : ¬∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ n
⊢ False
x : ℝ
hx : Liouville x
n : ℕ
⊢ ∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ n
refine Classical.not_not.1 fun H => ?_
x : ℝ
hx : Liouville x
n : ℕ
H : ∃ a, ∀ (b : ℕ), b ≥ a → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
⊢ False
x : ℝ
hx : Liouville x
n : ℕ
H : ¬∃ᶠ (b : ℕ) in atTop, ∃ a, x ≠ ↑a / ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ n
⊢ False
simp only [Liouville, not_forall, not_exists, not_frequently, not_and, not_lt,
  eventually_atTop] at H
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
⊢ False
x : ℝ
hx : Liouville x
n : ℕ
H : ∃ a, ∀ (b : ℕ), b ≥ a → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
⊢ False
rcases H with ⟨N, hN⟩
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
⊢ False
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
⊢ False
have : ∀ b > (1 : ℕ), ∀ᶠ m : ℕ in atTop, ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| := by
  intro b hb
  replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
  have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) := by
    simp only [one_div]
    exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
  refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
  exact fun m hm a => hm a
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
⊢ False
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
⊢ False
have : ∀ᶠ m : ℕ in atTop, ∀ b < N, 1 < b → ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
  (finite_lt_nat N).eventually_all.2 fun b _hb => eventually_imp_distrib_left.2 (this b)
case intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
⊢ False
case intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
⊢ False
rcases(this.and (eventually_ge_atTop n)).exists with ⟨m, hm, hnm⟩
case intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a b : ℤ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
⊢ False
case intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
⊢ False
rcases hx m with ⟨a, b, hb, hne, hlt⟩
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < ↑b
hne : x ≠ ↑a / ↑↑b
hlt : abs (x - ↑a / ↑↑b) < 1 / ↑↑b ^ m
⊢ False
case intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a b : ℤ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
⊢ False
lift b to ℕ using zero_le_one.trans hb.le
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑↑b
hlt : abs (x - ↑a / ↑↑b) < 1 / ↑↑b ^ m
hb : 1 < b
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < ↑b
hne : x ≠ ↑a / ↑↑b
hlt : abs (x - ↑a / ↑↑b) < 1 / ↑↑b ^ m
⊢ False
norm_cast  at hb
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑↑b
hlt : abs (x - ↑a / ↑↑b) < 1 / ↑↑b ^ m
hb : 1 < b
⊢ False
push_cast at hne hlt
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
⊢ False

case intro.intro.intro.intro.intro.intro.intro.intro.inr
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : b < N
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
⊢ False
cases' le_or_lt N b with h h
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : b > 1
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
⊢ ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
intro b hb
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : b > 1
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) := by
  simp only [one_div]
  exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ (x_1 : ℕ), (∀ (m : ℤ), 1 / ↑b ^ x_1 ≤ dist x (↑m / ↑b)) → ∀ (a : ℤ), 1 / ↑b ^ x_1 ≤ abs (x - ↑a / ↑b)
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
no goals
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
H : Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
⊢ ∀ (x_1 : ℕ), (∀ (m : ℤ), 1 / ↑b ^ x_1 ≤ dist x (↑m / ↑b)) → ∀ (a : ℤ), 1 / ↑b ^ x_1 ≤ abs (x - ↑a / ↑b)
exact fun m hm a => hm a
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m => (↑b ^ m)⁻¹) atTop (𝓝 0)
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m => 1 / ↑b ^ m) atTop (𝓝 0)
simp only [one_div]
no goals
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
b : ℕ
hb : 1 < ↑b
⊢ Tendsto (fun m => (↑b ^ m)⁻¹) atTop (𝓝 0)
exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
⊢ False
refine' (hN b h a hne).not_lt (hlt.trans_le _)
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
hb0 : 0 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
have hb0 : (0 : ℝ) < b := zero_lt_one.trans hb
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inl
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : N ≤ b
hb : 1 < ↑b
hb0 : 0 < ↑b
⊢ 1 / ↑b ^ m ≤ 1 / ↑b ^ n
exact one_div_le_one_div_of_le (pow_pos hb0 _) (pow_le_pow hb.le hnm)
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inr
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), b ≥ N → ∀ (x_1 : ℤ), x ≠ ↑x_1 / ↑b → 1 / ↑b ^ n ≤ abs (x - ↑x_1 / ↑b)
this✝ : ∀ (b : ℕ), b > 1 → ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
this : ∀ᶠ (m : ℕ) in atTop, ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
m : ℕ
hm : ∀ (b : ℕ), b < N → 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ abs (x - ↑a / ↑b)
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ ↑a / ↑b
hlt : abs (x - ↑a / ↑b) < 1 / ↑b ^ m
h : b < N
⊢ False
exact (hm b h hb _).not_lt hlt