awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : ℝ)|
b : ℕ
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
H : Tendsto (β := ℝ) (fun (m : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m) atTop (𝓝 0)
refine :
  ∀ (x_1 : ℕ),
    (∀ (m : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑b : ℝ))) →
      ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_

Premises used: Liouville.irrational, Filter.Eventually.mono, Irrational.eventually_forall_le_dist_cast_div, Filter.Tendsto.eventually
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : ℝ)|
b : ℕ
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
H : Tendsto (β := ℝ) (fun (m : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m) atTop (𝓝 0)
⊢ ∀ (x_1 : ℕ),
    (∀ (m : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑b : ℝ))) →
      ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
fun m hm a => hm a
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : ℝ)|
b : ℕ
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
H : Tendsto (β := ℝ) (fun (m : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m) atTop (𝓝 0)
⊢ ∀ (x_1 : ℕ),
    (∀ (m : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑b : ℝ))) →
      ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
exact fun m hm a => hm a
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : ℝ)|
⊢ ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
have : ∀ b > (1 : ℕ), ∀ᶠ m : ℕ in atTop, ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| := by
    intro b hb
    replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
    have H : Tendsto (fun m => 1 / (b : ℝ) ^ m : ℕ → ℝ) atTop (𝓝 0) := by
      simp only [one_div]
      exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)
    refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
    exact fun m hm a => hm a
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
⊢ ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
have : ∀ᶠ m : ℕ in atTop, ∀ b < N, 1 < b → ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
    (finite_lt_nat N).eventually_all.2 fun b _hb => eventually_imp_distrib_left.2 (this b)
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : ℝ)|
rcases :
  ∀ (m : ℕ)
    (hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|)
    (hnm : n ≤ m), False
⊢ False

Tactic:
rcases (this.and (eventually_ge_atTop n)).exists with ⟨m, hm, hnm⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_ge_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
rcases :
  ∀ (a b : ℤ) (hb : 1 < b) (hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
    (hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m), False
⊢ False

Tactic:
rcases hx m with ⟨a, b, hb, hne, hlt⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
⊢ 0 ≤ b

Tactic:
zero_le_one.trans hb.le

Premises used: LT.lt.le, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
lift :
  ∀ (b : ℕ) (hb : LT.lt (α := ℤ) 1 (↑b : ℤ)) (hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ))
    (hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) m), False
⊢ False

Tactic:
lift b to ℕ using zero_le_one.trans hb.le

Premises used: LT.lt.le, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : LT.lt (α := ℤ) 1 (↑b : ℤ)
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) m
⊢ 1 < b

Tactic:
norm_cast at hb
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
⊢ x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)

Tactic:
push_cast at hne hlt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : ℝ)
⊢ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m

Tactic:
push_cast at hne hlt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
inr : ∀ (h : b < N), False
⊢ False

Tactic:
rcases le_or_gt N b with h | h

Premises used: le_or_gt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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

Tactic:
(hN b h a hne).not_gt (hlt.trans_le ?_)

Premises used: LE.le.not_gt, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
inl : 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
⊢ False

Tactic:
refine (hN b h a hne).not_gt (hlt.trans_le ?_)

Premises used: LE.le.not_gt, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
inl : LE.le (α := ℝ) 1 (↑b : ℝ)
⊢ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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
⊢ LE.le (α := ℝ) 1 (↑b : ℝ)

Tactic:
exact_mod_cast hb.le

Premises used: LT.lt.le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : b < N
⊢ False

Tactic:
(hm b h hb _).not_gt hlt

Premises used: LE.le.not_gt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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 : b < N
⊢ False

Tactic:
exact (hm b h hb _).not_gt hlt

Premises used: LE.le.not_gt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
hx : Liouville x
p : ℝ
suffices : LiouvilleWith (↑⌈p⌉₊ : ℝ) x
⊢ LiouvilleWith p x

Tactic:
suffices LiouvilleWith ⌈p⌉₊ x from this.mono (Nat.le_ceil p)
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
hx : Liouville x
p : ℝ
⊢ LiouvilleWith (↑⌈p⌉₊ : ℝ) x

Tactic:
⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩

Premises used: LiouvilleWith, Liouville.frequently_exists_num, Filter.Frequently.mono, Nat.ceil, Exists.intro, Filter.Eventually.and_frequently, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
hx : Liouville x
p : ℝ
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⌉₊ : ℝ)
⊢ LiouvilleWith (↑⌈p⌉₊ : ℝ) x

Tactic:
refine ⟨1, ((eventually_gt_atTop 1).and_frequently (hx.frequently_exists_num ⌈p⌉₊)).mono ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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⌉₊ : ℝ)

Tactic:
⟨a, hne, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
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⌉₊
refine : |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⌉₊ : ℝ)

Tactic:
refine ⟨a, hne, ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
hx : Liouville x
p : ℝ
b : ℕ
_hb : 1 < b
a : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt rwa rwa₁ rwa₂ rwa₃ : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) ⌈p⌉₊
⊢ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (↑⌈p⌉₊ : ℝ)

Tactic:
rwa [rpow_natCast]

Premises used: Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x

Tactic:
⟨fun H n => ?_, Liouville.liouvilleWith⟩

Premises used: Liouville.liouvilleWith, Iff.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
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
⊢ (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x

Tactic:
refine ⟨fun H n => ?_, Liouville.liouvilleWith⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n : ℕ
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
⊢ ∃ (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⟩

Premises used: lt_add_one, Nat.cast, LiouvilleWith.frequently_lt_rpow_neg, Filter.Frequently.exists, HAdd.hAdd, Filter.Eventually.and_frequently, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑b : ℝ) (-(↑n : ℝ))
⊢ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) n

Tactic:
simpa [rpow_neg] using hlt

Premises used: Real.rpow_neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n 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:
exact ⟨a, b, mod_cast hb, hne, by simpa [rpow_neg] using hlt⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
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
⊢ 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⟩

Premises used: Iff.mpr, sub_pos, exists_nat_one_div_lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure
Goal:
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p - 2
⊢ 2 + 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < p

Tactic:
rw [lt_sub_iff_add_lt'] at hn

Premises used: lt_sub_iff_add_lt'