-- Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean
theorem volume_iUnion_setOf_liouvilleWith :
    volume (⋃ (p : ℝ) (_hp : 2 < p), { x : ℝ | LiouvilleWith p x }) = 0

Proof state:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ 2 < r

Tactic:
simp [← hr, zero_lt_one.trans_le hn]

Result:
no goals

Proof state:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ volume (B a b) = ↑(2 / ↑b ^ r)

Tactic:
rw [Real.volume_ball, mul_one_div, ← NNReal.coe_two, ← NNReal.coe_natCast, ← NNReal.coe_rpow,
  ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal]

Result:
no goals

Proof state:
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))

Tactic:
simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' this, mul_add,
  mul_left_comm]

Result:
no goals

Proof state:
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)))

Tactic:
have : 1 - r ≠ 0 := by linarith

Result:
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)))

Proof state:
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

Tactic:
linarith

Result:
no goals

Proof state:
⊢ volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0

Tactic:
simp only [← setOf_exists, exists_prop]

Result:
⊢ volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0

Proof state:
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 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Tactic:
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 ∈ 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_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_natCast]
    _ = _ := by
      have : 1 - r ≠ 0 := by linarith
      rw [ENNReal.coe_inj]
      simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' this, mul_add,
        mul_left_comm]

Result:
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 ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Proof state:
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 ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Tactic:
refine ne_top_of_le_ne_top (ENNReal.tsum_coe_ne_top_iff_summable.2 ?_) (ENNReal.tsum_le_tsum this)

Result:
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 ∈ Finset.Icc 0 ↑b, B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => 2 * (↑a ^ (1 - r) + ↑a ^ (-r))

Proof state:
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)))

Tactic:
rw [ENNReal.coe_inj]

Result:
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))

Proof state:
m : ℤ
⊢ volume
      ((fun x => x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
rw [measure_preimage_add_right]

Result:
m : ℤ
⊢ volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Proof state:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 < r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0

Tactic:
clear hn n

Result:
r : ℝ
hr : 2 < r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0

Proof state:
⊢ volume
      (⋃ m,
        (fun x => x + ↑m) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
rw [measure_iUnion_null_iff]

Result:
⊢ ∀ (i : ℤ),
    volume
        ((fun x => x + ↑i) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0

Proof state:
⊢ volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
refine (measure_biUnion_null_iff <| to_countable _).2 fun n (hn : 1 ≤ n) => ?_

Result:
n : ℕ
hn : 1 ≤ n
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)} = 0

Proof state:
r : ℝ
hr : 2 < r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0

Tactic:
refine measure_setOf_frequently_eq_zero ?_

Result:
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), volume {x | ∃ a ∈ Finset.Icc 0 ↑i, |x - ↑a / ↑i| < 1 / ↑i ^ r} ≠ ⊤

Proof state:
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Tactic:
set B : ℤ → ℕ → Set ℝ := fun a b => ball (a / b) (1 / (b : ℝ) ^ r)

Result:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Proof state:
n : ℕ
hn : 1 ≤ n
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)} = 0

Tactic:
generalize hr : (2 + 1 / n : ℝ) = r

Result:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0

Proof state:
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), volume {x | ∃ a ∈ Finset.Icc 0 ↑i, |x - ↑a / ↑i| < 1 / ↑i ^ r} ≠ ⊤

Tactic:
simp only [setOf_exists, ← exists_prop, ← Real.dist_eq, ← mem_ball, setOf_mem_eq]

Result:
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Proof state:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
⊢ ∑' (i : ℕ), volume (⋃ i_1 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Tactic:
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_natCast, ← NNReal.coe_rpow,
    ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal]

Result:
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 ∈ Finset.Icc 0 ↑i, ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤

Proof state:
⊢ volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0

Tactic:
refine measure_mono_null setOf_liouvilleWith_subset_aux ?_

Result:
⊢ volume
      (⋃ m,
        (fun x => x + ↑m) ⁻¹'
          ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0