⊢ ↑↑volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0
⊢ ↑↑volume (⋃ (p : ℝ) (_ : 2 < p), {x | LiouvilleWith p x}) = 0
simp only [← setOf_exists, exists_prop]
⊢ ↑↑volume
      (⋃ (m : ℤ),
        (fun x => x + ↑m) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
⊢ ↑↑volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0
refine' measure_mono_null setOf_liouvilleWith_subset_aux _
⊢ ∀ (i : ℤ),
    ↑↑volume
        ((fun x => x + ↑i) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0
⊢ ↑↑volume
      (⋃ (m : ℤ),
        (fun x => x + ↑m) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
rw [measure_iUnion_null_iff]
m : ℤ
⊢ ↑↑volume
      ((fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
⊢ ∀ (i : ℤ),
    ↑↑volume
        ((fun x => x + ↑i) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0
intro m
m : ℤ
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
m : ℤ
⊢ ↑↑volume
      ((fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
rw [measure_preimage_add_right]
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
m : ℤ
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
clear m
n : ℕ
hn : 1 ≤ n
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)} = 0
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
refine' (measure_biUnion_null_iff <| to_countable _).2 fun n (hn : 1 ≤ n) => _
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ r} = 0
n : ℕ
hn : 1 ≤ n
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ (2 + 1 / ↑n)} = 0
generalize hr : (2 + 1 / n : ℝ) = r
case hr
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ 2 < r

n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ r} = 0
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ r} = 0
replace hr : 2 < r
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ r} = 0
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ r} = 0
clear hn n
r : ℝ
hr : 2 < r
⊢ (∑' (i : ℕ), ↑↑volume {x | ∃ a, a ∈ Finset.Icc 0 ↑i ∧ abs (x - ↑a / ↑i) < 1 / ↑i ^ r}) ≠ ⊤
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ abs (x - ↑a / ↑b) < 1 / ↑b ^ r} = 0
refine' measure_setOf_frequently_eq_zero _
r : ℝ
hr : 2 < r
⊢ (∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r))) ≠ ⊤
r : ℝ
hr : 2 < r
⊢ (∑' (i : ℕ), ↑↑volume {x | ∃ a, a ∈ Finset.Icc 0 ↑i ∧ abs (x - ↑a / ↑i) < 1 / ↑i ^ r}) ≠ ⊤
simp only [setOf_exists, ← exists_prop, ← Real.dist_eq, ← mem_ball, setOf_mem_eq]
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))) ≠ ⊤
r : ℝ
hr : 2 < r
⊢ (∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r))) ≠ ⊤
set B : ℤ → ℕ → Set ℝ := fun a b => ball (a / b) (1 / (b : ℝ) ^ r)
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))) ≠ ⊤
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))) ≠ ⊤
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]
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))) ≠ ⊤
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))) ≠ ⊤
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]
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))
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))) ≠ ⊤
refine' ne_top_of_le_ne_top (ENNReal.tsum_coe_ne_top_iff_summable.2 _) (ENNReal.tsum_le_tsum this)
no goals
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))
refine' (Summable.add _ _).mul_left _ <;> simp only [NNReal.summable_rpow] <;> linarith
no goals
case hr
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ 2 < r
simp [← hr, zero_lt_one.trans_le hn]
no goals
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
rw [Real.volume_ball, mul_one_div, ← NNReal.coe_two, ← NNReal.coe_nat_cast, ← NNReal.coe_rpow,
  ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal]
no goals
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))
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]
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)))
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)))
have : 1 - r ≠ 0 := by linarith
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))
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)))
rw [ENNReal.coe_eq_coe]
no goals
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))
simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' _ this, mul_add,
  mul_left_comm]
no goals
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
linarith