awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ),
    (∃ (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 : ℝ) p
⊢ LiouvilleWith p (-x)

Tactic:
refine ⟨C, hC.mono ?_⟩
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ -x ≠ HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ)

Tactic:
simp [neg_div, hne]

Premises used: neg_div
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
refine : |-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 : ℝ) p

Tactic:
refine ⟨-m, by simp [neg_div, hne], ?_⟩
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
hlt
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
h : |-x - HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ)| = |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
⊢ |-x - HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
convert! hlt using 1
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
h : |HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ) - -x| = |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
⊢ |-x - HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ)| = |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|

Tactic:
rw [abs_sub_comm]

Premises used: abs_sub_comm
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
h : HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ) - -x = x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
⊢ |HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ) - -x| = |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|

Tactic:
congr! 1
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
h : HDiv.hDiv (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ) - -x = x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ) - -x = x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
push_cast
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ HDiv.hDiv (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ) - -x = x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
⊢ LiouvilleWith p (-x) ↔ LiouvilleWith p x

Tactic:
⟨fun h => neg_neg x ▸ h.neg, LiouvilleWith.neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, LiouvilleWith.neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
rw : LiouvilleWith p (x + -(↑r : ℝ)) ↔ LiouvilleWith p x
rw₁ : LiouvilleWith p (x + (↑(-r) : ℝ)) ↔ LiouvilleWith p x
rw₂ rw₃ : LiouvilleWith p x ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x - (↑r : ℝ)) ↔ LiouvilleWith p x

Tactic:
rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]

Premises used: sub_eq_add_neg, LiouvilleWith.add_rat_iff, Rat.cast_neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p (x - (↑r : ℝ))

Tactic:
sub_rat_iff.2 h

Premises used: Iff.mpr, LiouvilleWith.sub_rat_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
m : ℤ
rw : LiouvilleWith p (x - (↑(↑m : ℚ) : ℝ)) ↔ LiouvilleWith p x
rw₁ rw₂ : LiouvilleWith p x ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x - (↑m : ℝ)) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_intCast, sub_rat_iff]

Premises used: Rat.cast_intCast, LiouvilleWith.sub_rat_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
m : ℤ
⊢ LiouvilleWith p (x - (↑m : ℝ))

Tactic:
sub_int_iff.2 h

Premises used: Iff.mpr, LiouvilleWith.sub_int_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
n : ℕ
rw : LiouvilleWith p (x - (↑(↑n : ℚ) : ℝ)) ↔ LiouvilleWith p x
rw₁ rw₂ : LiouvilleWith p x ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x - (↑n : ℝ)) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_natCast, sub_rat_iff]

Premises used: Rat.cast_natCast, LiouvilleWith.sub_rat_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
n : ℕ
⊢ LiouvilleWith p (x - (↑n : ℝ))

Tactic:
sub_nat_iff.2 h

Premises used: Iff.mpr, LiouvilleWith.sub_nat_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p ((↑r : ℝ) - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p ((↑r : ℝ) - x)

Tactic:
rat_sub_iff.2 h

Premises used: Iff.mpr, LiouvilleWith.rat_sub_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p ((↑m : ℝ) - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
m : ℤ
⊢ LiouvilleWith p ((↑m : ℝ) - x)

Tactic:
int_sub_iff.2 h

Premises used: Iff.mpr, LiouvilleWith.int_sub_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p ((↑n : ℝ) - x) ↔ LiouvilleWith p x

Tactic:
simp [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
n : ℕ
⊢ LiouvilleWith p ((↑n : ℝ) - x)

Tactic:
nat_sub_iff.2 h

Premises used: Iff.mpr, LiouvilleWith.nat_sub_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
rcases :
  ∀ (n : ℕ) (hn : 0 < n) (m : ℤ) (hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
    (hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)), False
⊢ False

Tactic:
rcases ((eventually_gt_atTop 0).and_frequently (h.frequently_lt_rpow_neg hp)).exists with
    ⟨n : ℕ, hn : 0 < n, m : ℤ, hne : (M : ℝ) ≠ m / n, hlt : |(M - m / n : ℝ)| < n ^ (-1 : ℝ)⟩

Premises used: Int.cast, LiouvilleWith.frequently_lt_rpow_neg, Filter.Frequently.exists, Filter.Eventually.and_frequently, OfNat.ofNat, Neg.neg, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
⊢ False

Tactic:
hlt.not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
refine : HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) ≤ |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
⊢ False

Tactic:
refine hlt.not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
have hn' : (0 : ℝ) < n := by simpa
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
rw : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)| / (↑n : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) ≤ |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|

Tactic:
rw [rpow_neg_one, ← one_div, sub_div' hn'.ne', abs_div, Nat.abs_cast]

Premises used: Real.rpow_neg_one, Nat.abs_cast, abs_div, LT.lt.ne', one_div, sub_div'
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
hab : 1 ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)|
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)| / (↑n : ℝ)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
hab : 1 ≤ |M * (↑n : ℤ) - m|
⊢ 1 ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)|

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
hab : M * (↑n : ℤ) ≠ m
⊢ 1 ≤ |M * (↑n : ℤ) - m|

Tactic:
rw [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]

Premises used: sub_ne_zero, Int.add_one_le_iff, zero_add, abs_pos, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ¬HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) = (↑m : ℝ)

Tactic:
rw [Ne, eq_div_iff hn'.ne'] at hne

Premises used: Ne, LT.lt.ne', eq_div_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
hne₁ : ¬HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) = (↑m : ℝ)
⊢ |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)

Tactic:
rw [Ne, eq_div_iff hn'.ne'] at hne

Premises used: Ne, LT.lt.ne', eq_div_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
hne₁ : ¬HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) = (↑m : ℝ)
hlt₁ : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
rw [Ne, eq_div_iff hn'.ne'] at hne

Premises used: Ne, LT.lt.ne', eq_div_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : ¬HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) = (↑m : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ M * (↑n : ℤ) ≠ m

Tactic:
mod_cast hne

Premises used: Int.cast, Int.cast_natCast, HMul.hMul, congrArg, cast, Nat.cast, Int.cast_inj._simp_1, Int.cast_mul._simp_1, congrFun', Eq.symm, Eq, Not, Eq.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
n : ℕ
hn : 0 < n
m : ℤ
hne : ¬HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) = (↑m : ℝ)
hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ M * (↑n : ℤ) ≠ m

Tactic:
exact mod_cast hne
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
inl : ∀ (h : LiouvilleWith p (↑0 : ℝ)), False
inr : ∀ (h0 : r ≠ 0), False
⊢ False

Tactic:
rcases eq_or_ne r 0 with (rfl | h0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
h : LiouvilleWith p (↑0 : ℝ)
⊢ False

Tactic:
h.ne_cast_int hp 0 ?_

Premises used: LiouvilleWith.ne_cast_int, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
h : LiouvilleWith p (↑0 : ℝ)
inl : Eq (α := ℝ) (↑0 : ℝ) (↑0 : ℝ)
⊢ False

Tactic:
refine h.ne_cast_int hp 0 ?_

Premises used: LiouvilleWith.ne_cast_int, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
h : LiouvilleWith p (↑0 : ℝ)
inl : Eq (α := ℝ) 0 (↑0 : ℝ)
inl₁ inl₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) (↑0 : ℝ) (↑0 : ℝ)

Tactic:
rw [Rat.cast_zero, Int.cast_zero]

Premises used: Int.cast_zero, Rat.cast_zero
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
⊢ False

Tactic:
(h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_

Premises used: LiouvilleWith.mul_rat, LiouvilleWith.ne_cast_int, inv_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
inr : HMul.hMul (α := ℝ) (↑r : ℝ) (↑r⁻¹ : ℝ) = (↑1 : ℝ)
⊢ False

Tactic:
refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_

Premises used: LiouvilleWith.mul_rat, LiouvilleWith.ne_cast_int, inv_ne_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
inr : Eq (α := ℝ) 1 (↑1 : ℝ)
inr₁ : Ne (α := ℝ) (↑r : ℝ) 0
⊢ HMul.hMul (α := ℝ) (↑r : ℝ) (↑r⁻¹ : ℝ) = (↑1 : ℝ)

Tactic:
rw [Rat.cast_inv, mul_inv_cancel₀]

Premises used: mul_inv_cancel₀, Rat.cast_inv
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
⊢ Eq (α := ℝ) 1 (↑1 : ℝ)

Tactic:
Int.cast_one.symm

Premises used: Eq.symm, Int.cast_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
⊢ Ne (α := ℝ) (↑r : ℝ) 0

Tactic:
Rat.cast_ne_zero.mpr h0

Premises used: Iff.mpr, Rat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
⊢ Eq (α := ℝ) 1 (↑1 : ℝ)

Tactic:
exacts [Int.cast_one.symm, Rat.cast_ne_zero.mpr h0]

Premises used: Iff.mpr, Rat.cast_ne_zero, Eq.symm, Int.cast_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
hx : Liouville x
n : ℕ
by_contra! :
  ∀
    (H :
      ∀ᶠ (x_1 : ℕ) in atTop,
        ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑x_1 : ℝ)),
          1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑x_1 : ℝ)|),
    False
⊢ ∃ᶠ (b : ℕ) in atTop,
    ∃ (a : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n

Tactic:
by_contra! H
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
hx : Liouville x
n : ℕ
H :
  ∀ᶠ (x_1 : ℕ) in atTop,
    ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑x_1 : ℝ)),
      1 / HPow.hPow (α := ℝ) (↑x_1 : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑x_1 : ℝ)|
⊢ ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
        1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|

Tactic:
simp only [eventually_atTop] at H

Premises used: Filter.eventually_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
x : ℝ
hx : Liouville x
n : ℕ
H :
  ∃ (a : ℕ),
    ∀ b ≥ a,
      ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
        1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
rcases :
  ∀ (N : ℕ)
    (hN :
      ∀ b ≥ N,
        ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
          1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|),
    False
⊢ False

Tactic:
rcases H with ⟨N, hN⟩
-- 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 : b > 1
⊢ LT.lt (α := ℝ) 1 (↑b : ℝ)

Tactic:
replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 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 : ℝ)|
b : ℕ
hb : LT.lt (α := ℝ) 1 (↑b : ℝ)
simp : Tendsto (β := ℝ) (fun (m : ℕ) ↦ (HPow.hPow (α := ℝ) (↑b : ℝ) m)⁻¹) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m) atTop (𝓝 0)

Tactic:
simp only [one_div]

Premises used: one_div
-- 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 : ℝ)
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ (HPow.hPow (α := ℝ) (↑b : ℝ) m)⁻¹) atTop (𝓝 0)

Tactic:
tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)

Premises used: tendsto_inv_atTop_zero, tendsto_pow_atTop_atTop_of_one_lt, Filter.Tendsto.comp
-- 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 : ℝ)
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ (HPow.hPow (α := ℝ) (↑b : ℝ) m)⁻¹) atTop (𝓝 0)

Tactic:
exact tendsto_inv_atTop_zero.comp (tendsto_pow_atTop_atTop_of_one_lt hb)

Premises used: tendsto_inv_atTop_zero, tendsto_pow_atTop_atTop_of_one_lt, Filter.Tendsto.comp
-- 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 : ℝ)
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m) atTop (𝓝 0)

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

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