awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hdb : LE.le (α := ℝ) 1 (↑n : ℝ)
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ C / HPow.hPow (α := ℝ) (↑n : ℝ) q

Tactic:
gcongr
-- 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
⊢ LE.le (α := ℝ) 1 (↑n : ℝ)

Tactic:
exact_mod_cast hn
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt : 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),
    ∃ᶠ (n : ℕ) in atTop,
      ∃ (m : ℤ),
        x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
          |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)
⊢ ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)

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
hlt : 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 : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)

Tactic:
simpa only [(· ∘ ·), neg_sub, one_div] using
      ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_natCast_atTop_atTop).eventually
        (eventually_gt_atTop C)

Premises used: Iff.mpr, sub_pos, neg_sub, tendsto_rpow_atTop, Function.comp, tendsto_natCast_atTop_atTop, one_div, Filter.Tendsto.eventually, Filter.Tendsto.comp, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt : 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 : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)

Tactic:
have : ∀ᶠ n : ℕ in atTop, C < n ^ (p - q) := by
    simpa only [(· ∘ ·), neg_sub, one_div] using
      ((tendsto_rpow_atTop (sub_pos.2 hlt)).comp tendsto_natCast_atTop_atTop).eventually
        (eventually_gt_atTop C)
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt : 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
this : ∀ᶠ (n : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
⊢ ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)

Tactic:
(this.and_frequently hC).mono ?_

Premises used: Filter.Frequently.mono, Filter.Eventually.and_frequently
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt : 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
this : ∀ᶠ (n : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
refine :
  ∀ (x_1 : ℕ),
    (C < HPow.hPow (α := ℝ) (↑x_1 : ℝ) (p - q) ∧
        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 : ℝ)| < HPow.hPow (α := ℝ) (↑x_1 : ℝ) (-q)
⊢ ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)

Tactic:
refine (this.and_frequently hC).mono ?_

Premises used: Filter.Frequently.mono, Filter.Eventually.and_frequently
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt_1 : 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
this : ∀ᶠ (n : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
n : ℕ
hnC : C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
hn : 1 ≤ n
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ LT.lt (α := ℝ) 0 (↑n : ℝ)

Tactic:
replace hn : (0 : ℝ) < n := Nat.cast_pos.2 hn
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt_1 : 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
this : ∀ᶠ (n : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
n : ℕ
hnC : C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)

Tactic:
⟨m, hne, hlt.trans <| (div_lt_iff₀ <| rpow_pos_of_pos hn _).2 ?_⟩

Premises used: Iff.mpr, Real.rpow_pos_of_pos, div_lt_iff₀, And.intro, Exists.intro, LT.lt.trans
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt_1 : 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
this : ∀ᶠ (n : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
n : ℕ
hnC : C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
refine : C < HPow.hPow (α := ℝ) (↑n : ℝ) (-q) * HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)

Tactic:
refine ⟨m, hne, hlt.trans <| (div_lt_iff₀ <| rpow_pos_of_pos hn _).2 ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt_1 : 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
this : ∀ᶠ (n : ℕ) in atTop, C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
n : ℕ
hnC : C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
hn : LT.lt (α := ℝ) 0 (↑n : ℝ)
rwa : C < HPow.hPow (α := ℝ) (↑n : ℝ) p * HPow.hPow (α := ℝ) (↑n : ℝ) (-q)
rwa₁ : C < HPow.hPow (α := ℝ) (↑n : ℝ) (p + -q)
rwa₂ rwa₃ rwa₄ rwa₅ : C < HPow.hPow (α := ℝ) (↑n : ℝ) (p - q)
⊢ C < HPow.hPow (α := ℝ) (↑n : ℝ) (-q) * HPow.hPow (α := ℝ) (↑n : ℝ) p

Tactic:
rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, mul_comm, Real.rpow_add
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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 p (x * (↑r : ℝ))
⊢ LiouvilleWith p (x * (↑r : ℝ))

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

Premises used: LiouvilleWith.exists_pos
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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 p (x * (↑r : ℝ))

Tactic:
⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩

Premises used: Rat.pos, HMul.hMul, abs, Filter.tendsto_id, Filter.Tendsto.frequently, Rat.den, Rat.cast, LiouvilleWith, Nat.cast, Filter.Frequently.mono, Filter.Tendsto.nsmul_atTop, HPow.hPow, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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 * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id x_1) : ℝ) ∧
          |x * (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id x_1) : ℝ)| <
            HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id x_1) : ℝ) p
⊢ LiouvilleWith p (x * (↑r : ℝ))

Tactic:
refine ⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
⊢ HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)

Tactic:
simp [← div_mul_div_comm, ← r.cast_def, mul_comm]

Premises used: div_mul_div_comm, Rat.cast_def, mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
⊢ HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)

Tactic:
have A : (↑(r.num * m) : ℝ) / ↑(r.den • id n) = m / n * r := by
    simp [← div_mul_div_comm, ← r.cast_def, mul_comm]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ ∃ (m : ℤ),
    x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ) ∧
      |x * (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ)| <
        HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
⟨r.num * m, ?_, ?_⟩

Premises used: Rat.num, HMul.hMul, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_1 : x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ)
refine_2 :
  |x * (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
⊢ ∃ (m : ℤ),
    x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ) ∧
      |x * (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑(r.den • id n) : ℝ)| <
        HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
refine ⟨r.num * m, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_1 : x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ)

Tactic:
rw [A]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)

Tactic:
simp [hne, hr]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_2 :
  |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
⊢ |x * (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
rw [A, ← sub_mul, abs_mul]

Premises used: abs_mul, sub_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_2 :
  |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
⊢ |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
simp only [smul_eq_mul, id, Nat.cast_mul]

Premises used: id, Nat.cast_mul, smul_eq_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
ha : LT.lt (α := ℝ) 0 |(↑r : ℝ)|
⊢ |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)|

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p

Tactic:
?_
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_2 :
  C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
⊢ |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p

Tactic:
calc _ < C / ↑n ^ p * |↑r| := by gcongr
      _ = ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p := ?_

Premises used: HMul.hMul, Rat.den
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
refine_2 : |(↑r : ℝ)| * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p) = (↑|r| : ℝ) * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p)
refine_2₁ : HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0
refine_2₂ : LE.le (α := ℝ) 0 (↑r.den : ℝ)
refine_2₃ : LE.le (α := ℝ) 0 (↑n : ℝ)
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p * |(↑r : ℝ)| =
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p

Tactic:
rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]

Premises used: mul_div_assoc, Real.mul_rpow, mul_div_mul_left, mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ |(↑r : ℝ)| * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p) = (↑|r| : ℝ) * (C / HPow.hPow (α := ℝ) (↑n : ℝ) p)

Tactic:
simp only [Rat.cast_abs]

Premises used: Rat.cast_abs
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
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
A : HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ) = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
⊢ LE.le (α := ℝ) 0 (↑r.den : ℝ)

Tactic:
positivity