awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 0 < m
k : ℕ
zero : ∃ (p : ℕ), partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ 0!) : ℝ)
succ :
  ∀ (k : ℕ) (h : ∃ (p : ℕ), partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ k !) : ℝ)),
    ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ k !) : ℝ)

Tactic:
induction k with
  | zero => exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]⟩
  | succ k h =>
    rcases h with ⟨p_k, h_k⟩
    use p_k * m ^ ((k + 1)! - k !) + 1
    rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
    · norm_cast
      rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
      simp [mul_assoc]
    all_goals positivity

Premises used: add_mul, Nat.factorial_succ, mul_assoc, HSub.hSub, pow_add, div_eq_div_iff, HAdd.hAdd, Nat.factorial, div_add_div, LiouvilleNumber.partialSum_succ, add_tsub_cancel_right, OfNat.ofNat, one_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 < m
⊢ LT.lt (α := ℤ) 1 (↑m : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
⊢ LT.lt (α := ℤ) 1 (↑m : ℤ)

Tactic:
have mZ1 : 1 < (m : ℤ) := by norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 < m
⊢ LT.lt (α := ℝ) 1 (↑m : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
⊢ LT.lt (α := ℝ) 1 (↑m : ℝ)

Tactic:
have m1 : 1 < (m : ℝ) := by norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n : ℕ
rcases :
  ∀ (p : ℕ) (hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)),
    ∃ (a : ℤ) (b : ℤ),
      1 < b ∧
        liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
          |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
⊢ ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n

Tactic:
rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩

Premises used: LiouvilleNumber.partialSum_eq_rat, LT.lt.trans_le, zero_lt_two
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)
⊢ ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n

Tactic:
⟨p, m ^ n !, one_lt_pow₀ mZ1 n.factorial_ne_zero, ?_⟩

Premises used: Nat.cast, Nat.factorial_ne_zero, HPow.hPow, Nat.factorial, And.intro, Exists.intro, one_lt_pow₀
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)
refine :
  liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) ∧
    |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ)| <
      1 / HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) n
⊢ ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n

Tactic:
refine ⟨p, m ^ n !, one_lt_pow₀ mZ1 n.factorial_ne_zero, ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)
push_cast :
  liouvilleNumber (↑m : ℝ) ≠ (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ∧
    |liouvilleNumber (↑m : ℝ) - (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n
⊢ liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) ∧
    |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ)| <
      1 / HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) n

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)
⊢ partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !

Tactic:
rw [Nat.cast_pow] at hp

Premises used: Nat.cast_pow
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
rw :
  partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n ≠ partialSum (↑m : ℝ) n ∧
    |partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n - partialSum (↑m : ℝ) n| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n
⊢ liouvilleNumber (↑m : ℝ) ≠ (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ∧
    |liouvilleNumber (↑m : ℝ) - (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n

Tactic:
rw [← partialSum_add_remainder m1 n, ← hp]

Premises used: LiouvilleNumber.partialSum_add_remainder
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
⊢ 0 < remainder (↑m : ℝ) n

Tactic:
have hpos := remainder_pos m1 n
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
hpos : 0 < remainder (↑m : ℝ) n
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ :
  ∀ (mZ1 m1 : 1 < m) (hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ))
    (hpos : 0 < remainder (↑m : ℝ) n), 2 ≤ m
⊢ LE.le (α := ℝ) 2 (↑m : ℝ)

Tactic:
assumption_mod_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
hpos : 0 < remainder (↑m : ℝ) n
⊢ partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n ≠ partialSum (↑m : ℝ) n ∧
    |partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n - partialSum (↑m : ℝ) n| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n

Tactic:
simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)

Premises used: LT.lt.ne', abs_of_pos, LiouvilleNumber.remainder_lt
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
Goal:
m : ℕ
hm : 2 ≤ m
⊢ Transcendental ℤ (liouvilleNumber (↑m : ℝ))

Tactic:
(liouville_liouvilleNumber hm).transcendental

Premises used: liouville_liouvilleNumber, Liouville.transcendental
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
h :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
⊢ LiouvilleWith 1 x

Tactic:
use 2
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
⊢ ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1

Tactic:
((eventually_gt_atTop 0).mono fun n hn => ?_).frequently

Premises used: Filter.Eventually.mono, Filter.Eventually.frequently, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
h :
  ∀ (n : ℕ) (hn : 0 < n),
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
⊢ ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1

Tactic:
refine ((eventually_gt_atTop 0).mono fun n hn => ?_).frequently

Premises used: Filter.Eventually.mono, Filter.Eventually.frequently, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hn' : (0 : ℝ) < n := by simpa
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : x * (↑n : ℝ) < HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1
⊢ x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)

Tactic:
rw [lt_div_iff₀ hn', Int.cast_add, Int.cast_one]

Premises used: lt_div_iff₀, Int.cast_add, Int.cast_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ x * (↑n : ℝ) < HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1

Tactic:
Int.lt_floor_add_one _

Premises used: Int.lt_floor_add_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ x * (↑n : ℝ) < HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1

Tactic:
exact Int.lt_floor_add_one _

Premises used: Int.lt_floor_add_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)

Tactic:
have : x < ↑(⌊x * ↑n⌋ + 1) / ↑n := by
    rw [lt_div_iff₀ hn', Int.cast_add, Int.cast_one]
    exact Int.lt_floor_add_one _
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1

Tactic:
⟨⌊x * n⌋ + 1, this.ne, ?_⟩

Premises used: HMul.hMul, Int.floor, Nat.cast, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, LT.lt.ne
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
h : |x - HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1

Tactic:
refine ⟨⌊x * n⌋ + 1, this.ne, ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
h : HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ) < (x * (↑n : ℝ) + 2) / (↑n : ℝ)
⊢ |x - HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1

Tactic:
rw [abs_sub_comm, abs_of_pos (sub_pos.2 this), rpow_one, sub_lt_iff_lt_add',
    add_div_eq_mul_add_div _ _ hn'.ne']

Premises used: Iff.mpr, sub_pos, sub_lt_iff_lt_add', Real.rpow_one, LT.lt.ne', abs_sub_comm, abs_of_pos, add_div_eq_mul_add_div
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
h : (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) < x * (↑n : ℝ) + 2
⊢ HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ) < (x * (↑n : ℝ) + 2) / (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
push_cast : HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1 ≤ x * (↑n : ℝ) + 1
⊢ (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) ≤ x * (↑n : ℝ) + 1

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
bc : (↑⌊x * (↑n : ℝ)⌋ : ℝ) ≤ x * (↑n : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1 ≤ x * (↑n : ℝ) + 1

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ (↑⌊x * (↑n : ℝ)⌋ : ℝ) ≤ x * (↑n : ℝ)

Tactic:
apply Int.floor_le

Premises used: Int.floor_le
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
linarith : x * (↑n : ℝ) + 2 ≤ x * (↑n : ℝ) + 1 → -1 + (x * (↑n : ℝ) + 2 - (x * (↑n : ℝ) + 1)) = 0
⊢ x * (↑n : ℝ) + 1 < x * (↑n : ℝ) + 2

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
calc : (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) ≤ x * (↑n : ℝ) + 1
calc₁ : x * (↑n : ℝ) + 1 < x * (↑n : ℝ) + 2
⊢ (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) < x * (↑n : ℝ) + 2

Tactic:
calc _ ≤ x * n + 1 := by push_cast; gcongr; apply Int.floor_le
    _ < x * n + 2 := by linarith
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
rcases :
  ∀ (C : ℝ)
    (hC :
      ∃ᶠ (n : ℕ) in atTop,
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p),
    ∃ (C : ℝ) (_ : 0 < C),
      ∃ᶠ (n : ℕ) in atTop,
        1 ≤ n ∧
          ∃ (m : ℤ),
            x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
              |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ ∃ (C : ℝ) (_ : 0 < C),
    ∃ᶠ (n : ℕ) in atTop,
      1 ≤ n ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
rcases h with ⟨C, hC⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ ∃ (C : ℝ) (_ : 0 < C),
    ∃ᶠ (n : ℕ) in atTop,
      1 ≤ n ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩

Premises used: le_max_right, zero_lt_one, Max.max, LT.lt.trans_le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
refine :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ ∃ (C : ℝ) (_ : 0 < C),
    ∃ᶠ (n : ℕ) in atTop,
      1 ≤ n ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
refine ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
((eventually_ge_atTop 1).and_frequently hC).mono ?_

Premises used: Filter.Frequently.mono, Filter.eventually_ge_atTop, Filter.Eventually.and_frequently, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
refine :
  ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ)| < C / HPow.hPow (α := ℝ) (↑x_1 : ℝ) p) →
      1 ≤ x_1 ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ)| < max C 1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) p
⊢ ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
refine ((eventually_ge_atTop 1).and_frequently hC).mono ?_

Premises used: Filter.Frequently.mono, Filter.eventually_ge_atTop, Filter.Eventually.and_frequently, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ 1 ≤ n ∧
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
⟨hle, m, hne, hlt.trans_le ?_⟩

Premises used: LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
refine : C / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ 1 ≤ n ∧
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
refine ⟨hle, m, hne, hlt.trans_le ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
hab : C ≤ max C 1
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x C : ℝ
hC :
  ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hle : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ C ≤ max C 1

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
rcases :
  ∀ (C : ℝ) (hC₀ : 0 < C)
    (hC :
      ∃ᶠ (n : ℕ) in atTop,
        1 ≤ n ∧
          ∃ (m : ℤ),
            x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
              |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p),
    LiouvilleWith q x
⊢ LiouvilleWith q x

Tactic:
rcases h.exists_pos with ⟨C, hC₀, hC⟩

Premises used: LiouvilleWith.exists_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ LiouvilleWith q x

Tactic:
⟨C, hC.mono ?_⟩

Premises used: LiouvilleWith, Filter.Frequently.mono, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
refine :
  ∀ (x_1 : ℕ),
    (1 ≤ x_1 ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ)| < C / HPow.hPow (α := ℝ) (↑x_1 : ℝ) p) →
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑x_1 : ℝ)| < C / HPow.hPow (α := ℝ) (↑x_1 : ℝ) q
⊢ LiouvilleWith q x

Tactic:
refine ⟨C, hC.mono ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) q

Tactic:
⟨m, hne, hlt.trans_le <| ?_⟩

Premises used: LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
C : ℝ
hC₀ : 0 < C
hC :
  ∃ᶠ (n : ℕ) in atTop,
    1 ≤ n ∧
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
n : ℕ
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
refine : C / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ C / HPow.hPow (α := ℝ) (↑n : ℝ) q
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) q

Tactic:
refine ⟨m, hne, hlt.trans_le <| ?_⟩