awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : Membership.mem (γ := Set ℝ) (Ico 0 1) x
b : ℕ
a : ℤ
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
hlt : x * (↑b : ℝ) - 1 < (↑a : ℝ) ∧ (↑a : ℝ) < 1 + x * (↑b : ℝ)
⊢ 1 + x * (↑b : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)
have refine_2 : x * (↑b : ℝ) ≤ (↑b : ℝ)
Tactic: rw [add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (p : ℝ), ⋃ (_ : 2 < p), {x : ℝ | LiouvilleWith p x}) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | ∃ (i : ℝ), 2 < i ∧ LiouvilleWith i x} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [← setOf_exists, exists_prop]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | ∃ (i : ℝ), 2 < i ∧ LiouvilleWith i x} : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : 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: refine measure_mono_null setOf_liouvilleWith_subset_aux ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
⊢ 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∞)
have 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∞)
Tactic: rw [measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
m : ℤ
⊢ 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∞)
have 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∞)
Tactic: rw [measure_preimage_add_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
have 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∞)
Tactic: refine (measure_biUnion_null_iff <| to_countable _).2 fun n (hn : 1 ≤ n) => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
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∞)
have 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∞)
Tactic: generalize hr : (2 + 1 / n : ℝ) = r
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
Goal:
n : ℕ
hn : 1 ≤ n
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∞)
have hr₁ : 2 < r
Tactic: replace hr : 2 < r := by simp [← hr, zero_lt_one.trans_le hn]
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
have 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})
  ∞
Tactic: refine measure_setOf_frequently_eq_zero ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
r : ℝ
hr : 2 < 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})
    ∞
have 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)))
  ∞
Tactic: simp only [setOf_exists, ← exists_prop, ← Real.dist_eq, ← mem_ball, setOf_mem_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
have rw : ENNReal.ofReal (2 * (1 / HPow.hPow (α := ℝ) (↑b : ℝ) r)) = (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
have rw₁ : ENNReal.ofReal (2 / HPow.hPow (α := ℝ) (↑b : ℝ) r) = (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
have rw₂ : ENNReal.ofReal ((↑2 : ℝ) / HPow.hPow (α := ℝ) (↑b : ℝ) r) = (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
have rw₃ : ENNReal.ofReal ((↑2 : ℝ) / (↑(↑b : ℝ≥0) : ℝ) ^ r) = (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
have rw₄ : ENNReal.ofReal ((↑2 : ℝ) / (↑(HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ)) =
  (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
have rw₅ : ENNReal.ofReal (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ) = (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
⊢ (volume : (a : Set ℝ) → ℝ≥0∞) (B a b) = (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞)
have rw₆ : (↑(2 / HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) r) : ℝ≥0∞) = (↑(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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
Goal:
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ :=
  fun (a : ℤ) (b : ℕ) ↦ ball (HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)) (1 / HPow.hPow (α := ℝ) (↑b : ℝ) 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)))
    ∞
have hB : ∀ (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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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
have linarith : 1 - r = 0 → -1 + (2 - r) + -(1 - r - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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 : ℕ
⊢ (↑(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∞)
have this : 1 - r ≠ 0
Tactic: have : 1 - r ≠ 0 := by linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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)) : ℝ≥0∞) =
    (↑(2 * (HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑b : ℝ≥0) (-r))) : ℝ≥0∞)
have 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))
Tactic: rw [ENNReal.coe_inj]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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∞)
⊢ 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)))
    ∞
have 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∞)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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)))
    ∞
have refine : Summable (α := ℝ≥0) fun (a : ℕ) ↦ 2 * (HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r))
Tactic: refine ne_top_of_le_ne_top (ENNReal.tsum_coe_ne_top_iff_summable.2 ?_) (ENNReal.tsum_le_tsum this)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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))
have refine_1 : Summable (α := ℝ≥0) fun (a : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r)
Tactic: refine (Summable.add ?_ ?_).mul_left _
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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)
⊢ Summable (α := ℝ≥0) fun (a : ℕ) ↦ 2 * (HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r) + HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r))
have refine_2 : Summable (α := ℝ≥0) fun (a : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r)
Tactic: refine (Summable.add ?_ ?_).mul_left _
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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 : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (1 - r)
have refine_1 : 1 - r < -1
Tactic: simp only [NNReal.summable_rpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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 : ℕ) ↦ HPow.hPow (α := ℝ≥0) (↑a : ℝ≥0) (-r)
have refine_2 : -r < -1
Tactic: simp only [NNReal.summable_rpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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∞)
⊢ 1 - r < -1
have linarith : -1 ≤ 1 - r → 2 - r + (-1 - (1 - r)) = 0
Tactic: linarith