[GOAL]
⊢ {x | ∃ p, p > 2 ∧ LiouvilleWith p x} ⊆
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
rintro x ⟨p, hp, hxp⟩
[GOAL]
case intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
rcases exists_nat_one_div_lt (sub_pos.2 hp) with ⟨n, hn⟩
[GOAL]
case intro.intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 1 / (↑n + 1) < p - 2
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
rw [lt_sub_iff_add_lt'] at hn 
[GOAL]
case intro.intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
suffices
  ∀ y : ℝ,
    LiouvilleWith p y →
      y ∈ Ico (0 : ℝ) 1 →
        ∃ᶠ b : ℕ in atTop, ∃ a ∈ Finset.Icc (0 : ℤ) b, |y - a / b| < 1 / (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ)
  by
  simp only [mem_iUnion, mem_preimage]
  have hx : x + ↑(-⌊x⌋) ∈ Ico (0 : ℝ) 1 := by
    simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff, mem_Ico,
      Int.cast_neg, le_add_neg_iff_add_le]
  refine' ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
simp only [mem_iUnion, mem_preimage]
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ ∃ i i_1 i_2, x + ↑i ∈ {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑i_1)}
[PROOFSTEP]
have hx : x + ↑(-⌊x⌋) ∈ Ico (0 : ℝ) 1 := by
  simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff, mem_Ico, Int.cast_neg,
    le_add_neg_iff_add_le]
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ x + ↑(-⌊x⌋) ∈ Ico 0 1
[PROOFSTEP]
simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff, mem_Ico, Int.cast_neg,
  le_add_neg_iff_add_le]
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
hx : x + ↑(-⌊x⌋) ∈ Ico 0 1
⊢ ∃ i i_1 i_2, x + ↑i ∈ {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑i_1)}
[PROOFSTEP]
refine' ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
[GOAL]
case intro.intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
clear hxp x
[GOAL]
case intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
intro x hxp hx01
[GOAL]
case intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
⊢ ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
refine' ((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono _
[GOAL]
case intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < ↑x_1 ^ (-(2 + 1 / (↑n + 1)))) ∧ 1 ≤ x_1 →
      ∃ a, a ∈ Finset.Icc 0 ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
rintro b ⟨⟨a, -, hlt⟩, hb⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < ↑b ^ (-(2 + 1 / (↑n + 1)))
⊢ ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
rw [rpow_neg b.cast_nonneg, ← one_div, ← Nat.cast_succ] at hlt 
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
⊢ ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
refine' ⟨a, _, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
replace hb : (1 : ℝ) ≤ b
[GOAL]
case hb
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
⊢ 1 ≤ ↑b
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
exact Nat.one_le_cast.2 hb
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
have hb0 : (0 : ℝ) < b := zero_lt_one.trans_le hb
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
replace hlt : |x - a / b| < 1 / b
[GOAL]
case hlt
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ |x - ↑a / ↑b| < 1 / ↑b
[PROOFSTEP]
refine' hlt.trans_le (one_div_le_one_div_of_le hb0 _)
[GOAL]
case hlt
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ ↑b ≤ ↑b ^ (2 + 1 / ↑(Nat.succ n))
[PROOFSTEP]
calc
  (b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
  _ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) := rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)
[GOAL]
case hlt
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ 2 ≤ 2 + 1 / ↑(n + 1)
[PROOFSTEP]
simpa using n.cast_add_one_pos.le
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
rw [sub_div' _ _ _ hb0.ne', abs_div, abs_of_pos hb0, div_lt_div_right hb0, abs_sub_lt_iff, sub_lt_iff_lt_add,
  sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt 
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
rw [Finset.mem_Icc, ← Int.lt_add_one_iff, ← Int.lt_add_one_iff, ← neg_lt_iff_pos_add, add_comm, ← @Int.cast_lt ℝ, ←
  @Int.cast_lt ℝ]
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ ↑(-1) < ↑a ∧ ↑a < ↑(1 + ↑b)
[PROOFSTEP]
push_cast
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ -1 < ↑a ∧ ↑a < 1 + ↑b
[PROOFSTEP]
refine' ⟨lt_of_le_of_lt _ hlt.1, hlt.2.trans_le _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ -1 ≤ x * ↑b - 1
[PROOFSTEP]
simp only [mul_nonneg hx01.left b.cast_nonneg, neg_le_sub_iff_le_add, le_add_iff_nonneg_left]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ 1 + x * ↑b ≤ 1 + ↑b
[PROOFSTEP]
rw [add_le_add_iff_left]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ x * ↑b ≤ ↑b
[PROOFSTEP]
exact mul_le_of_le_one_left hb0.le hx01.2.le
[GOAL]
⊢ ↑↑volume (⋃ (p : ℝ) (_ : 2 < p), {x | LiouvilleWith p x}) = 0
[PROOFSTEP]
simp only [← setOf_exists, exists_prop]
[GOAL]
⊢ ↑↑volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0
[PROOFSTEP]
refine' measure_mono_null setOf_liouvilleWith_subset_aux _
[GOAL]
⊢ ↑↑volume
      (⋃ (m : ℤ),
        (fun x => x + ↑m) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
rw [measure_iUnion_null_iff]
[GOAL]
⊢ ∀ (i : ℤ),
    ↑↑volume
        ((fun x => x + ↑i) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0
[PROOFSTEP]
intro m
[GOAL]
m : ℤ
⊢ ↑↑volume
      ((fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
rw [measure_preimage_add_right]
[GOAL]
m : ℤ
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
clear m
[GOAL]
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
refine' (measure_biUnion_null_iff <| to_countable _).2 fun n (hn : 1 ≤ n) => _
[GOAL]
n : ℕ
hn : 1 ≤ n
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)} = 0
[PROOFSTEP]
generalize hr : (2 + 1 / n : ℝ) = r
[GOAL]
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
[PROOFSTEP]
replace hr : 2 < r
[GOAL]
case hr
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ 2 < r
[PROOFSTEP]
simp [← hr, zero_lt_one.trans_le hn]
[GOAL]
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
[PROOFSTEP]
clear hn n
[GOAL]
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
[PROOFSTEP]
refine' measure_setOf_frequently_eq_zero _
[GOAL]
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), ↑↑volume {x | ∃ a, a ∈ Finset.Icc 0 ↑i ∧ |x - ↑a / ↑i| < 1 / ↑i ^ r} ≠ ⊤
[PROOFSTEP]
simp only [setOf_exists, ← exists_prop, ← Real.dist_eq, ← mem_ball, setOf_mem_eq]
[GOAL]
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
set B : ℤ → ℕ → Set ℝ := fun a b => ball (a / b) (1 / (b : ℝ) ^ r)
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
have hB : ∀ a b, volume (B a b) = ↑((2 : ℝ≥0) / (b : ℝ≥0) ^ r) := fun a b ↦ by
  rw [Real.volume_ball, mul_one_div, ← NNReal.coe_two, ← NNReal.coe_nat_cast, ← NNReal.coe_rpow, ← NNReal.coe_div,
    ENNReal.ofReal_coe_nnreal]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
[PROOFSTEP]
rw [Real.volume_ball, mul_one_div, ← NNReal.coe_two, ← NNReal.coe_nat_cast, ← NNReal.coe_rpow, ← NNReal.coe_div,
  ENNReal.ofReal_coe_nnreal]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
have : ∀ b : ℕ, volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤ ↑(2 * ((b : ℝ≥0) ^ (1 - r) + (b : ℝ≥0) ^ (-r))) := fun b ↦
  calc
    volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤ ∑ a in Finset.Icc (0 : ℤ) b, volume (B a b) :=
      measure_biUnion_finset_le _ _
    _ = ↑((b + 1) * (2 / (b : ℝ≥0) ^ r)) := by
      simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero, ← Int.ofNat_succ, Int.toNat_coe_nat, ←
        Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_nat]
    _ = _ := by
      have : 1 - r ≠ 0 := by linarith
      rw [ENNReal.coe_eq_coe]
      simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' _ this, mul_add, mul_left_comm]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ ∑ a in Finset.Icc 0 ↑b, ↑↑volume (B a b) = ↑((↑b + 1) * (2 / ↑b ^ r))
[PROOFSTEP]
simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero, ← Int.ofNat_succ, Int.toNat_coe_nat, ←
  Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_nat]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ ↑((↑b + 1) * (2 / ↑b ^ r)) = ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
[PROOFSTEP]
have : 1 - r ≠ 0 := by linarith
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ 1 - r ≠ 0
[PROOFSTEP]
linarith
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
this : 1 - r ≠ 0
⊢ ↑((↑b + 1) * (2 / ↑b ^ r)) = ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
[PROOFSTEP]
rw [ENNReal.coe_eq_coe]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
this : 1 - r ≠ 0
⊢ (↑b + 1) * (2 / ↑b ^ r) = 2 * (↑b ^ (1 - r) + ↑b ^ (-r))
[PROOFSTEP]
simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' _ this, mul_add, mul_left_comm]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
refine' ne_top_of_le_ne_top (ENNReal.tsum_coe_ne_top_iff_summable.2 _) (ENNReal.tsum_le_tsum this)
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => 2 * (↑a ^ (1 - r) + ↑a ^ (-r))
[PROOFSTEP]
refine' (Summable.add _ _).mul_left _
[GOAL]
case refine'_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => ↑a ^ (1 - r)
[PROOFSTEP]
simp only [NNReal.summable_rpow]
[GOAL]
case refine'_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => ↑a ^ (-r)
[PROOFSTEP]
simp only [NNReal.summable_rpow]
[GOAL]
case refine'_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ 1 - r < -1
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ -r < -1
[PROOFSTEP]
linarith
[GOAL]
⊢ ∀ᵐ (x : ℝ), ∀ (p : ℝ), p > 2 → ¬LiouvilleWith p x
[PROOFSTEP]
simpa only [ae_iff, not_forall, Classical.not_not, setOf_exists] using volume_iUnion_setOf_liouvilleWith
[GOAL]
x : ℝ
h₁ : ∀ (p : ℝ), p > 2 → ¬LiouvilleWith p x
h₂ : Liouville x
⊢ 3 > 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ ↑↑volume {x | Liouville x} = 0
[PROOFSTEP]
simpa only [ae_iff, Classical.not_not] using ae_not_liouville
