awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      Membership.mem (γ := Set ℝ) (Ico 0 1) y →
        ∃ᶠ (b : ℕ) in atTop,
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
              |y - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
simp :
  ∃ (i : ℤ) (i_1 : ℕ) (_ : i_1 > 0),
    Membership.mem (γ := Set ℝ)
      {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 (↑i_1 : ℝ))}
      (x + (↑i : ℝ))
⊢ Membership.mem (γ := Set ℝ)
    (⋃ (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 : ℝ))}))
    x

Tactic:
simp only [mem_iUnion, mem_preimage]

Premises used: Set.mem_iUnion, Set.mem_preimage
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      Membership.mem (γ := Set ℝ) (Ico 0 1) y →
        ∃ᶠ (b : ℕ) in atTop,
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
              |y - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
⊢ Membership.mem (γ := Set ℝ) (Ico 0 1) (x + (↑(-⌊x⌋) : ℝ))

Tactic:
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]

Premises used: Int.cast_neg, Set.mem_Ico, Int.lt_floor_add_one, le_add_neg_iff_add_le, add_neg_lt_iff_le_add', zero_add, Int.floor_le, and_self_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      Membership.mem (γ := Set ℝ) (Ico 0 1) y →
        ∃ᶠ (b : ℕ) in atTop,
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
              |y - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
⊢ Membership.mem (γ := Set ℝ) (Ico 0 1) (x + (↑(-⌊x⌋) : ℝ))

Tactic:
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]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      Membership.mem (γ := Set ℝ) (Ico 0 1) y →
        ∃ᶠ (b : ℕ) in atTop,
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
              |y - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
hx : Membership.mem (γ := Set ℝ) (Ico 0 1) (x + (↑(-⌊x⌋) : ℝ))
⊢ ∃ (i : ℤ) (i_1 : ℕ) (_ : i_1 > 0),
    Membership.mem (γ := Set ℝ)
      {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 (↑i_1 : ℝ))}
      (x + (↑i : ℝ))

Tactic:
⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩

Premises used: Int.floor, LiouvilleWith.add_int, HAdd.hAdd, Nat.succ_pos, Exists.intro, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      Membership.mem (γ := Set ℝ) (Ico 0 1) y →
        ∃ᶠ (b : ℕ) in atTop,
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
              |y - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
hx : Membership.mem (γ := Set ℝ) (Ico 0 1) (x + (↑(-⌊x⌋) : ℝ))
⊢ ∃ (i : ℤ) (i_1 : ℕ) (_ : i_1 > 0),
    Membership.mem (γ := Set ℝ)
      {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 (↑i_1 : ℝ))}
      (x + (↑i : ℝ))

Tactic:
exact ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
suffices :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      Membership.mem (γ := Set ℝ) (Ico 0 1) y →
        ∃ᶠ (b : ℕ) in atTop,
          ∃ (a : ℤ),
            Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
              |y - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
                1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
⊢ Membership.mem (γ := Set ℝ)
    (⋃ (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 : ℝ))}))
    x

Tactic:
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]
    exact ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℕ) 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 + 1) : ℝ))

Tactic:
((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono ?_

Premises used: Filter.Frequently.mono, LiouvilleWith.frequently_lt_rpow_neg, Filter.Frequently.and_eventually, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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
refine :
  ∀ (x_1 : ℕ),
    (∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ)| <
              HPow.hPow (α := ℝ) (↑x_1 : ℝ) (-(2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))) ∧
        1 ≤ x_1 →
      ∃ (a : ℤ),
        Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑x_1 : ℤ)) a ∧
          |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑x_1 : ℝ)| <
            1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
⊢ ∃ᶠ (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 + 1) : ℝ))

Tactic:
refine ((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono ?_

Premises used: Filter.Frequently.mono, LiouvilleWith.frequently_lt_rpow_neg, Filter.Frequently.and_eventually, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℕ
hb : 1 ≤ b
a : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < HPow.hPow (α := ℝ) (↑b : ℝ) (-(2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1))
⊢ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))

Tactic:
rw [rpow_neg b.cast_nonneg, ← one_div, ← Nat.cast_succ] at hlt

Premises used: Nat.cast_succ, Nat.cast_nonneg, one_div, Real.rpow_neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℕ
hb : 1 ≤ b
a : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
⊢ ∃ (a : ℤ),
    Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
      |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
        1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))

Tactic:
⟨a, ?_, hlt⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℕ
hb : 1 ≤ b
a : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
refine : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a
⊢ ∃ (a : ℤ),
    Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
      |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
        1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))

Tactic:
refine ⟨a, ?_, hlt⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℕ
hb : 1 ≤ b
a : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
⊢ LE.le (α := ℝ) 1 (↑b : ℝ)

Tactic:
replace hb : (1 : ℝ) ≤ b := Nat.one_le_cast.2 hb
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑b : ℝ)

Tactic:
have hb0 : (0 : ℝ) < b := zero_lt_one.trans_le hb
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)

Tactic:
hlt.trans_le (one_div_le_one_div_of_le hb0 ?_)

Premises used: one_div_le_one_div_of_le, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
refine : (↑b : ℝ) ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
⊢ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)

Tactic:
refine hlt.trans_le (one_div_le_one_div_of_le hb0 ?_)

Premises used: one_div_le_one_div_of_le, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ (↑b : ℝ) = HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) 1

Tactic:
(rpow_one _).symm

Premises used: Real.rpow_one, Eq.symm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) 1 ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))

Tactic:
rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)

Premises used: one_le_two, LE.le.trans, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
_ : 2 ≤ 2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
⊢ (↑b : ℝ) ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))

Tactic:
calc
      (b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
      _ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) :=
        rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)

Premises used: HDiv.hDiv, Nat.cast, Real.rpow_one, HAdd.hAdd, one_le_two, LE.le.trans, OfNat.ofNat, Eq.symm, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ 2 ≤ 2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
simpa using n.cast_add_one_pos.le

Premises used: Nat.cast_add_one_pos, LT.lt.le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℤ
hlt :
  |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
hb : LE.le (α := ℝ) 1 (↑b : ℝ)
hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
⊢ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)

Tactic:
replace hlt : |x - a / b| < 1 / b := by
    refine hlt.trans_le (one_div_le_one_div_of_le hb0 ?_)
    calc
      (b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
      _ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) :=
        rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)
    simpa using n.cast_add_one_pos.le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)
⊢ x * (↑b : ℝ) - 1 < (↑a : ℝ) ∧ (↑a : ℝ) < 1 + x * (↑b : ℝ)

Tactic:
rw [sub_div' hb0.ne', abs_div, abs_of_pos hb0, div_lt_div_iff_of_pos_right hb0, abs_sub_lt_iff,
    sub_lt_iff_lt_add, sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt

Premises used: div_lt_div_iff_of_pos_right, abs_div, abs_sub_lt_iff, sub_lt_iff_lt_add', LT.lt.ne', sub_lt_iff_lt_add, abs_of_pos, sub_div'
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ)
rw : LT.lt (α := ℝ) (↑(-1) : ℝ) (↑a : ℝ) ∧ LT.lt (α := ℝ) (↑a : ℝ) (↑(HAdd.hAdd (α := ℤ) 1 (↑b : ℤ)) : ℝ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a

Tactic:
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 ℝ]

Premises used: Finset.mem_Icc, Int.cast_lt, add_comm, neg_lt_iff_pos_add, Int.lt_add_one_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ)
push_cast : LT.lt (α := ℝ) (-1) (↑a : ℝ) ∧ (↑a : ℝ) < HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)
⊢ LT.lt (α := ℝ) (↑(-1) : ℝ) (↑a : ℝ) ∧ LT.lt (α := ℝ) (↑a : ℝ) (↑(HAdd.hAdd (α := ℤ) 1 (↑b : ℤ)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ)
⊢ LT.lt (α := ℝ) (-1) (↑a : ℝ) ∧ (↑a : ℝ) < HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)

Tactic:
⟨lt_of_le_of_lt ?_ hlt.1, hlt.2.trans_le ?_⟩

Premises used: lt_of_le_of_lt, And.right, And.left, LT.lt.trans_le, And.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ)
refine_1 : -1 ≤ x * (↑b : ℝ) - 1
refine_2 : 1 + x * (↑b : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)
⊢ LT.lt (α := ℝ) (-1) (↑a : ℝ) ∧ (↑a : ℝ) < HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)

Tactic:
refine ⟨lt_of_le_of_lt ?_ hlt.1, hlt.2.trans_le ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ) - 1

Tactic:
simp only [mul_nonneg hx01.left b.cast_nonneg, neg_le_sub_iff_le_add, le_add_iff_nonneg_left]

Premises used: mul_nonneg, Nat.cast_nonneg, And.left, neg_le_sub_iff_le_add, le_add_iff_nonneg_left
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ)
refine_2 : x * (↑b : ℝ) ≤ (↑b : ℝ)
⊢ 1 + x * (↑b : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)

Tactic:
rw [add_le_add_iff_left]

Premises used: add_le_add_iff_left
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ)
⊢ x * (↑b : ℝ) ≤ (↑b : ℝ)

Tactic:
mul_le_of_le_one_left hb0.le hx01.2.le

Premises used: LT.lt.le, mul_le_of_le_one_left, And.right
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
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 : ℝ)
⊢ x * (↑b : ℝ) ≤ (↑b : ℝ)

Tactic:
exact mul_le_of_le_one_left hb0.le hx01.2.le

Premises used: LT.lt.le, mul_le_of_le_one_left, And.right
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
simp : Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | ∃ (i : ℝ), 2 < i ∧ LiouvilleWith i x} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (⋃ (p : ℝ), ⋃ (_ : 2 < p), {x : ℝ | LiouvilleWith p x}) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp only [← setOf_exists, exists_prop]

Premises used: Set.setOf_exists, exists_prop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | ∃ (i : ℝ), 2 < i ∧ LiouvilleWith i x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null setOf_liouvilleWith_subset_aux ?_

Premises used: setOf_liouvilleWith_subset_aux, MeasureTheory.measure_mono_null
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
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∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) {x : ℝ | ∃ (i : ℝ), 2 < i ∧ LiouvilleWith i x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null setOf_liouvilleWith_subset_aux ?_

Premises used: setOf_liouvilleWith_subset_aux, MeasureTheory.measure_mono_null