awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
Goal:
x : ℝ
hx : Liouville x
n N : ℕ
hN :
  ∀ b ≥ N,
    ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
      1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) m
hb : 1 < b
⊢ False
have hne₁ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
Tactic: push_cast at hne hlt
Cleared hypotheses: hne, hlt
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
Goal:
x : ℝ
hx : Liouville x
n N : ℕ
hN :
  ∀ b ≥ N,
    ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
      1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a : ℤ
b : ℕ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) m
hb : 1 < b
hne₁ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
⊢ False
have hlt₁ : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m
Tactic: push_cast at hne hlt
Cleared hypotheses: hne, hlt
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
n N : ℕ
hN :
  ∀ b ≥ N,
    ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
      1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m
⊢ False
have inl : ∀ (h : N ≤ b), False
Tactic: rcases le_or_gt N b with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
n N : ℕ
hN :
  ∀ b ≥ N,
    ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
      1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m
inl : ∀ (h : N ≤ b), False
⊢ False
have inr : ∀ (h : b < N), False
Tactic: rcases le_or_gt N b with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
n N : ℕ
hN :
  ∀ b ≥ N,
    ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
      1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m
h : N ≤ b
⊢ False
have inl : 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
Tactic: refine (hN b h a hne).not_gt (hlt.trans_le ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
n N : ℕ
hN :
  ∀ b ≥ N,
    ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
      1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : 1 < b
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m
h : N ≤ b
⊢ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
have inl : LE.le (α := ℝ) 1 (↑b : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith p x
have suffices : LiouvilleWith (↑⌈p⌉₊ : ℝ) x
Tactic: suffices LiouvilleWith ⌈p⌉₊ x from this.mono (Nat.le_ceil p)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊ : ℝ) x
have refine : ∀ (x_1 : ℕ),
  (1 < x_1 ∧
      ∃ (a : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑x_1 : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑x_1 : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) ⌈p⌉₊) →
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℝ) (↑x_1 : ℝ) (↑⌈p⌉₊ : ℝ)
Tactic: refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) ⌈p⌉₊
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑b : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈p⌉₊ : ℝ)
have refine : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈p⌉₊ : ℝ)
Tactic: refine ⟨a, hne, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x
have refine : ∀ (H : ∀ (p : ℝ), LiouvilleWith p x) (n : ℕ),
  ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
Tactic: refine ⟨fun H n => ?_, Liouville.liouvilleWith⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
⊢ ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
have rcases : ∀ (b : ℕ) (hb : 1 < b) (a : ℤ) (hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
  (hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (-(↑n : ℝ))),
  ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
Tactic: rcases ((eventually_gt_atTop 1).and_frequently
    ((H (n + 1)).frequently_lt_rpow_neg (lt_add_one (n : ℝ)))).exists
    with ⟨b, hb, a, hne, hlt⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
⊢ 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
have rcases : ∀ (n : ℕ) (hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p - 2),
  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: rcases exists_nat_one_div_lt (sub_pos.2 hp) with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p - 2
⊢ 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
have hn₁ : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
Tactic: rw [lt_sub_iff_add_lt'] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
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 ℝ)
    (⋃ (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
have 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 : ℝ))
Tactic: simp only [mem_iUnion, mem_preimage]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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) : ℝ))
⊢ ∃ (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 : ℝ))
have hx : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (goal)
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p
⊢ 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
have 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) : ℝ))
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⟩
-- 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 : ℕ) 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) : ℝ))
have 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) : ℝ))
Tactic: refine ((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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))
⊢ ∃ (a : ℤ),
    Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a ∧
      |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| <
        1 / HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ))
have hlt₁ : |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
Cleared hypotheses: hlt
-- 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 : ℕ
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) : ℝ))
have refine : Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a
Tactic: refine ⟨a, ?_, hlt⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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 : ℝ))
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a
have hb₁ : LE.le (α := ℝ) 1 (↑b : ℝ)
Tactic: replace hb : (1 : ℝ) ≤ b := Nat.one_le_cast.2 hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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 : ℝ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a
have hb0 : LT.lt (α := ℝ) 0 (↑b : ℝ)
Tactic: have hb0 : (0 : ℝ) < b := zero_lt_one.trans_le hb
-- 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 : ℤ
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 : ℝ)
have refine : (↑b : ℝ) ≤ HPow.hPow (α := ℝ) (↑b : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
Tactic: refine hlt.trans_le (one_div_le_one_div_of_le hb0 ?_)
-- 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 : ℤ
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 : ℝ) (2 + HDiv.hDiv (α := ℝ) 1 (↑n.succ : ℝ))
have _ : 2 ≤ 2 + HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
Tactic: calc
      (b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
      _ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) :=
        rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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 : ℝ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a
have hlt₁ : |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
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Measure (hypothesis)
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 : ℝ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a
have hlt₁ : 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
Cleared hypotheses: hlt
-- 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 : ℝ)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc 0 (↑b : ℤ)) a
have rw : LT.lt (α := ℝ) (↑(-1) : ℝ) (↑a : ℝ) ∧ LT.lt (α := ℝ) (↑a : ℝ) (↑(HAdd.hAdd (α := ℤ) 1 (↑b : ℤ)) : ℝ)
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 ℝ]
-- 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 : ℝ)
⊢ LT.lt (α := ℝ) (↑(-1) : ℝ) (↑a : ℝ) ∧ LT.lt (α := ℝ) (↑a : ℝ) (↑(HAdd.hAdd (α := ℤ) 1 (↑b : ℤ)) : ℝ)
have push_cast : LT.lt (α := ℝ) (-1) (↑a : ℝ) ∧ (↑a : ℝ) < HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)
Tactic: push_cast
-- 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 : ℝ)
⊢ LT.lt (α := ℝ) (-1) (↑a : ℝ) ∧ (↑a : ℝ) < HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)
have refine_1 : -1 ≤ x * (↑b : ℝ) - 1
Tactic: refine ⟨lt_of_le_of_lt ?_ hlt.1, hlt.2.trans_le ?_⟩
-- 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 : ℝ)
refine_1 : -1 ≤ x * (↑b : ℝ) - 1
⊢ LT.lt (α := ℝ) (-1) (↑a : ℝ) ∧ (↑a : ℝ) < HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)
have refine_2 : 1 + x * (↑b : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 (↑b : ℝ)
Tactic: refine ⟨lt_of_le_of_lt ?_ hlt.1, hlt.2.trans_le ?_⟩