awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
rw :
  ∀ (i : ℤ),
    Eq (α := ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞)
          (preimage (β := ℝ) (fun (x : ℝ) ↦ x + (↑i : ℝ))
            (⋃ (n : ℕ),
              ⋃ (_ : n > 0),
                {x : ℝ |
                  ∃ᶠ (b : ℕ) in atTop,
                    ∃ (a : ℤ),
                      Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                          1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))})) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (m : ℤ),
          preimage (β := ℝ) (fun (x : ℝ) ↦ x + (↑m : ℝ))
            (⋃ (n : ℕ),
              ⋃ (_ : n > 0),
                {x : ℝ |
                  ∃ᶠ (b : ℕ) in atTop,
                    ∃ (a : ℤ),
                      Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                          1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))})) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [measure_iUnion_null_iff]

Premises used: MeasureTheory.measure_iUnion_null_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
m : ℤ
rw :
  Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (n : ℕ),
          ⋃ (_ : n > 0),
            {x : ℝ |
              ∃ᶠ (b : ℕ) in atTop,
                ∃ (a : ℤ),
                  Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                    |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                      1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (preimage (β := ℝ) (fun (x : ℝ) ↦ x + (↑m : ℝ))
          (⋃ (n : ℕ),
            ⋃ (_ : n > 0),
              {x : ℝ |
                ∃ᶠ (b : ℕ) in atTop,
                  ∃ (a : ℤ),
                    Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                      |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                        1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))})) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [measure_preimage_add_right]

Premises used: MeasureTheory.measure_preimage_add_right
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (n : ℕ),
          ⋃ (_ : n > 0),
            {x : ℝ |
              ∃ᶠ (b : ℕ) in atTop,
                ∃ (a : ℤ),
                  Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                    |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                      1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

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

Premises used: Iff.mpr, Set.Mem, Set.to_countable, MeasureTheory.measure_biUnion_null_iff, Nat.lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
refine :
  ∀ (n : ℕ) (hn : 1 ≤ n),
    Eq (α := ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞)
          {x : ℝ |
            ∃ᶠ (b : ℕ) in atTop,
              ∃ (a : ℤ),
                Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                    1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (n : ℕ),
          ⋃ (_ : n > 0),
            {x : ℝ |
              ∃ᶠ (b : ℕ) in atTop,
                ∃ (a : ℤ),
                  Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                    |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                      1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))}) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

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

Premises used: Iff.mpr, Set.to_countable, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
n : ℕ
hn : 1 ≤ n
generalize :
  ∀ (r : ℝ) (hr : 2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = r),
    Eq (α := ℝ≥0∞)
      ((volume : (a : Set ℝ) → ℝ≥0∞)
          {x : ℝ |
            ∃ᶠ (b : ℕ) in atTop,
              ∃ (a : ℤ),
                Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) r} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        {x : ℝ |
          ∃ᶠ (b : ℕ) in atTop,
            ∃ (a : ℤ),
              Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                  1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

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

Premises used: HDiv.hDiv, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = r
⊢ 2 < r

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

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = r
⊢ 2 < r

Tactic:
replace hr : 2 < r := by simp [← hr, zero_lt_one.trans_le hn]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        {x : ℝ |
          ∃ᶠ (b : ℕ) in atTop,
            ∃ (a : ℤ),
              Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) r} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
measure_setOf_frequently_eq_zero ?_

Premises used: MeasureTheory.measure_setOf_frequently_eq_zero
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
refine :
  Ne (α := ℝ≥0∞)
    (∑' (i : ℕ),
      (volume : (a : Set ℝ) → ℝ≥0∞)
        {x : ℝ |
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑i : ℤ)) a ∧
              |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑i : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑i : ℝ) r})
    ∞
⊢ Eq (α := ℝ≥0∞)
    ((volume : (a : Set ℝ) → ℝ≥0∞)
        {x : ℝ |
          ∃ᶠ (b : ℕ) in atTop,
            ∃ (a : ℤ),
              Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
                |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) r} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
refine measure_setOf_frequently_eq_zero ?_

Premises used: MeasureTheory.measure_setOf_frequently_eq_zero
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
simp :
  Ne (α := ℝ≥0∞)
    (∑' (i : ℕ),
      (volume : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i_1 : ℤ),
          ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑i : ℤ)) i_1),
            ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i : ℝ) r)))
    ∞
⊢ Ne (α := ℝ≥0∞)
    (∑' (i : ℕ),
      (volume : (a : Set ℝ) → ℝ≥0∞)
        {x : ℝ |
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑i : ℤ)) a ∧
              |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑i : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑i : ℝ) r})
    ∞

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

Premises used: Set.setOf_exists, exists_prop, Metric.mem_ball, Set.setOf_mem_eq, Real.dist_eq
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
a : ℤ
b : ℕ
rw : ENNReal.ofReal (2 * (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
rw₁ : ENNReal.ofReal (2 / HPow.hPow (α := ℝ) (↑b : ℝ) r) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
rw₂ : ENNReal.ofReal ((↑2 : ℝ) / HPow.hPow (α := ℝ) (↑b : ℝ) r) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
rw₃ : ENNReal.ofReal ((↑2 : ℝ) / (↑(↑b : ℝ≥0) : ℝ) ^ r) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
rw₄ :
  ENNReal.ofReal ((↑2 : ℝ) / (↑(HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ)) =
    (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
rw₅ : ENNReal.ofReal (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
rw₆ rw₇ : (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)

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

Premises used: NNReal.coe_div, NNReal.coe_rpow, Real.volume_ball, NNReal.coe_natCast, NNReal.coe_two, mul_one_div, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
⊢ ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)

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]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
b : ℕ
⊢ ∑ a ∈ Finset.Icc 0 (↑b : ℤ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) =
    (↑(HAdd.hAdd (α := ℝ≥0) (↑b : ℝ≥0) 1 * (2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r)) : ℝ≥0∞)

Tactic:
simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero,
          Int.toNat_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_natCast]

Premises used: Nat.cast_succ, Int.toNat_natCast, sub_zero, ENNReal.coe_mul, Int.card_Icc, nsmul_eq_mul, ENNReal.coe_natCast, Finset.sum_const
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
b : ℕ
linarith : 1 - r = 0 → -1 + (2 - r) + -(1 - r - 0) = 0
⊢ 1 - r ≠ 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
b : ℕ
⊢ 1 - r ≠ 0

Tactic:
have : 1 - r ≠ 0 := by linarith
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
b : ℕ
this : 1 - r ≠ 0
rw :
  HAdd.hAdd (α := ℝ≥0) (↑b : ℝ≥0) 1 * (2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) =
    2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))
⊢ (↑(HAdd.hAdd (α := ℝ≥0) (↑b : ℝ≥0) 1 * (2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r)) : ℝ≥0∞) =
    (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_inj]

Premises used: ENNReal.coe_inj
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
b : ℕ
this : 1 - r ≠ 0
⊢ HAdd.hAdd (α := ℝ≥0) (↑b : ℝ≥0) 1 * (2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) =
    2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))

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

Premises used: add_mul, NNReal.rpow_sub', mul_left_comm, div_eq_mul_inv, NNReal.rpow_neg, mul_add
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
⊢ ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)

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.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]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞)
    (∑' (i : ℕ),
      (volume : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i_1 : ℤ),
          ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑i : ℤ)) i_1),
            ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i : ℝ) r)))
    ∞

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

Premises used: Iff.mpr, ENNReal.tsum_le_tsum, ne_top_of_le_ne_top, ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
refine :
  Summable (α := ℝ≥0) fun (a : ℕ) ↦ 2 * (HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r))
⊢ Ne (α := ℝ≥0∞)
    (∑' (i : ℕ),
      (volume : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (i_1 : ℤ),
          ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑i : ℤ)) i_1),
            ball (HDiv.hDiv (α := ℝ) (↑i_1 : ℝ) (↑i : ℝ)) (1 / HPow.hPow (α := ℝ) (↑i : ℝ) r)))
    ∞

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

Premises used: Iff.mpr, ENNReal.tsum_le_tsum, ne_top_of_le_ne_top, ENNReal.tsum_coe_ne_top_iff_summable
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
⊢ Summable (α := ℝ≥0) fun (a : ℕ) ↦ 2 * (HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r))

Tactic:
(Summable.add ?_ ?_).mul_left _

Premises used: Summable.add, Summable.mul_left
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
refine_1 : Summable (α := ℝ≥0) fun (a : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r)
refine_2 : Summable (α := ℝ≥0) fun (a : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r)
⊢ Summable (α := ℝ≥0) fun (a : ℕ) ↦ 2 * (HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r))

Tactic:
refine (Summable.add ?_ ?_).mul_left _

Premises used: Summable.add, Summable.mul_left
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
refine_1 : 1 - r < -1
⊢ Summable (α := ℝ≥0) fun (a : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r)

Tactic:
simp only [NNReal.summable_rpow]

Premises used: NNReal.summable_rpow
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
refine_2 : -r < -1
⊢ Summable (α := ℝ≥0) fun (a : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r)

Tactic:
simp only [NNReal.summable_rpow]

Premises used: NNReal.summable_rpow
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
linarith : -1 ≤ 1 - r → 2 - r + (-1 - (1 - r)) = 0
⊢ 1 - r < -1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)
hB : ∀ (a : ℤ) (b : ℕ), (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
this :
  ∀ (b : ℕ),
    (volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (a : ℤ), ⋃ (_ : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a), B a b) ≤
      (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
linarith : -1 ≤ -r → -1 + (2 - r) + (-1 - -r) = 0
⊢ -r < -1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
⊢ ∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x

Tactic:
simpa only [ae_iff, not_forall, Classical.not_not, setOf_exists] using
    volume_iUnion_setOf_liouvilleWith

Premises used: volume_iUnion_setOf_liouvilleWith, Classical.not_not, Set.setOf_exists, MeasureTheory.ae_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x : ℝ
h₁ : ∀ p > 2, ¬LiouvilleWith p x
h₂ : Liouville x
⊢ GT.gt (α := ℝ) 3 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | Liouville x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa only [ae_iff, Classical.not_not] using ae_not_liouville

Premises used: Classical.not_not, MeasureTheory.ae_iff, ae_not_liouville
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
⊢ Disjoint (residual ℝ) (ae (F := Measure ℝ) volume)

Tactic:
disjoint_of_disjoint_of_mem disjoint_compl_right eventually_residual_liouville ae_not_liouville

Premises used: Filter.disjoint_of_disjoint_of_mem, disjoint_compl_right, ae_not_liouville, eventually_residual_liouville
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
h :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) {x : ℝ | Liouville x} x ↔
      Membership.mem (γ := Set ℝ)
        (⋂ (n : ℕ),
          ⋃ (a : ℤ),
            ⋃ (b : ℤ),
              ⋃ (_ : 1 < b),
                ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
                  {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
        x
⊢ Eq (α := Set ℝ) {x : ℝ | Liouville x}
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
x : ℝ
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | Liouville x} x ↔
    Membership.mem (γ := Set ℝ)
      (⋂ (n : ℕ),
        ⋃ (a : ℤ),
          ⋃ (b : ℤ),
            ⋃ (_ : 1 < b),
              ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
                {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
      x

Tactic:
simp only [mem_iInter, mem_iUnion, Liouville, mem_setOf_eq, exists_prop, mem_diff,
    mem_singleton_iff, mem_ball, Real.dist_eq, and_comm]

Premises used: Set.mem_iUnion, Set.mem_setOf_eq, Liouville, and_comm, exists_prop, Set.mem_iInter, Metric.mem_ball, Set.mem_singleton_iff, Real.dist_eq, Set.mem_diff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
rw :
  IsGδ (X := ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})
⊢ IsGδ (X := ℝ) {x : ℝ | Liouville x}

Tactic:
rw [setOf_liouville_eq_iInter_iUnion]

Premises used: setOf_liouville_eq_iInter_iUnion
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual
Goal:
⊢ IsGδ (X := ℝ)
    (⋂ (n : ℕ),
      ⋃ (a : ℤ),
        ⋃ (b : ℤ),
          ⋃ (_ : 1 < b),
            ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) n) \
              {HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)})

Tactic:
.iInter fun n => IsOpen.isGδ ?_

Premises used: IsGδ.iInter, IsOpen.isGδ