x : ℝ
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
x : ℝ
⊢ LiouvilleWith 1 x
use 2
x : ℝ
n : ℕ
hn : 0 < n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
x : ℝ
⊢ ∃ᶠ (n : ℕ) in atTop, ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
refine ((eventually_gt_atTop 0).mono fun n hn => ?_).frequently
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
x : ℝ
n : ℕ
hn : 0 < n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
have hn' : (0 : ℝ) < n := by simpa
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
have : x < ↑(⌊x * ↑n⌋ + 1) / ↑n := by
  rw [lt_div_iff hn', Int.cast_add, Int.cast_one];
  exact Int.lt_floor_add_one _
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ abs (x - ↑(⌊x * ↑n⌋ + 1) / ↑n) < 2 / ↑n ^ 1
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ∃ m, x ≠ ↑m / ↑n ∧ abs (x - ↑m / ↑n) < 2 / ↑n ^ 1
refine ⟨⌊x * n⌋ + 1, this.ne, ?_⟩
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) < x * ↑n + 2
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ abs (x - ↑(⌊x * ↑n⌋ + 1) / ↑n) < 2 / ↑n ^ 1
rw [abs_sub_comm, abs_of_pos (sub_pos.2 this), rpow_one, sub_lt_iff_lt_add',
  add_div_eq_mul_add_div _ _ hn'.ne', div_lt_div_right hn']
no goals
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ ↑(⌊x * ↑n⌋ + 1) < x * ↑n + 2
convert add_lt_add_right ((Int.floor_le (x * n)).trans_lt (lt_add_one _)) 1 using 1 <;>
push_cast <;> ring
no goals
x : ℝ
n : ℕ
hn : 0 < n
⊢ 0 < ↑n
simpa
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x * ↑n < ↑⌊x * ↑n⌋ + 1
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x < ↑(⌊x * ↑n⌋ + 1) / ↑n
rw [lt_div_iff hn', Int.cast_add, Int.cast_one]
no goals
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x * ↑n < ↑⌊x * ↑n⌋ + 1
exact Int.lt_floor_add_one _