awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
hr : r ≠ 0
h : LiouvilleWith p (x * (↑r : ℝ))
⊢ LiouvilleWith p x

Tactic:
simpa only [mul_assoc, ← Rat.cast_mul, mul_inv_cancel₀ hr, Rat.cast_one, mul_one] using
      h.mul_rat (inv_ne_zero hr)

Premises used: Rat.cast_mul, mul_inv_cancel₀, mul_assoc, LiouvilleWith.mul_rat, inv_ne_zero, mul_one, Rat.cast_one
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
hr : r ≠ 0
rw : LiouvilleWith p (x * (↑r : ℝ)) ↔ LiouvilleWith p x
rw₁ rw₂ : LiouvilleWith p x ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑r : ℝ) * x) ↔ LiouvilleWith p x

Tactic:
rw [mul_comm, mul_rat_iff hr]

Premises used: LiouvilleWith.mul_rat_iff, mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
⊢ LiouvilleWith p ((↑r : ℝ) * x)

Tactic:
(rat_mul_iff hr).2 h

Premises used: Iff.mpr, LiouvilleWith.rat_mul_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
m : ℤ
hm : m ≠ 0
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, mul_rat_iff (Int.cast_ne_zero.2 hm)]

Premises used: Iff.mpr, Rat.cast_intCast, LiouvilleWith.mul_rat_iff, Int.cast_ne_zero
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
m : ℤ
h : LiouvilleWith p x
hm : m ≠ 0
⊢ LiouvilleWith p (x * (↑m : ℝ))

Tactic:
(mul_int_iff hm).2 h

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

Tactic:
rw [mul_comm, mul_int_iff hm]

Premises used: LiouvilleWith.mul_int_iff, mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
m : ℤ
h : LiouvilleWith p x
hm : m ≠ 0
⊢ LiouvilleWith p ((↑m : ℝ) * x)

Tactic:
(int_mul_iff hm).2 h

Premises used: Iff.mpr, LiouvilleWith.int_mul_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
n : ℕ
hn : n ≠ 0
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, mul_rat_iff (Nat.cast_ne_zero.2 hn)]

Premises used: Iff.mpr, LiouvilleWith.mul_rat_iff, Rat.cast_natCast, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * (↑n : ℝ))

Tactic:
(mul_nat_iff hn).2 h

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

Tactic:
rw [mul_comm, mul_nat_iff hn]

Premises used: mul_comm, LiouvilleWith.mul_nat_iff
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
rw : LiouvilleWith p (x * (↑n : ℝ))
⊢ LiouvilleWith p ((↑n : ℝ) * x)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * (↑n : ℝ))

Tactic:
h.mul_nat hn

Premises used: LiouvilleWith.mul_nat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
n : ℕ
h : LiouvilleWith p x
hn : n ≠ 0
⊢ LiouvilleWith p (x * (↑n : ℝ))

Tactic:
exact h.mul_nat hn

Premises used: LiouvilleWith.mul_nat
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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 : ℝ
h : LiouvilleWith p x
r : ℚ
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 * C, (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩

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

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

Tactic:
rw [smul_eq_mul, id]

Premises used: id, smul_eq_mul
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
nth_rewrite :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den * n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑(HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ)) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den * n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)

Tactic:
nth_rewrite 4 [← Rat.num_div_den r]

Premises used: Rat.num_div_den
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
push_cast :
  (HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) + HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ)) /
      HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den * n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑(HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ)) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
⊢ Ne (α := ℝ) (↑r.den : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
rw :
  HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) +
      HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
rw₁ :
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) +
      HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
rw₂ rw₃ :
  HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)
⊢ (HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑m : ℝ) + HMul.hMul (α := ℝ) (↑r.num : ℝ) (↑n : ℝ)) /
      HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑r.num : ℝ) (↑r.den : ℝ)

Tactic:
rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]

Premises used: mul_div_mul_right, mul_div_mul_left, add_div
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)

Tactic:
have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r := by
    rw [smul_eq_mul, id]
    nth_rewrite 4 [← Rat.num_div_den r]
    push_cast
    rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(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 * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

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

Premises used: Rat.num, HMul.hMul, Rat.den, Nat.cast, HAdd.hAdd, Exists.intro
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
refine :
  x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) ∧
    |x + (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ)| <
      HPow.hPow (α := ℝ) (↑r.den : ℝ) p * 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 * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
refine ⟨r.den * m + r.num * n, ?_⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
rw :
  x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ) ∧
    |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| <
      HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
⊢ x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) ∧
    |x + (↑r : ℝ) - HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ)| <
      HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
rw [this, add_sub_add_right_eq_sub]

Premises used: add_sub_add_right_eq_sub
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
⊢ x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)

Tactic:
simpa
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
refine :
  C / HPow.hPow (α := ℝ) (↑n : ℝ) p = HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
⊢ x + (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ) ∧
    |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| <
      HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
refine ⟨by simpa, hlt.trans_le (le_of_eq ?_)⟩
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(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 : ℝ
h : LiouvilleWith p x
r : ℚ
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
this :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
⊢ HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0

Tactic:
have : (r.den ^ p : ℝ) ≠ 0 := by positivity
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
r : ℚ
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
this_1 :
  HDiv.hDiv (α := ℝ) (↑((↑r.den : ℤ) * m + r.num * (↑n : ℤ)) : ℝ) (↑(r.den • id n) : ℝ) =
    HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) + (↑r : ℝ)
this : HPow.hPow (α := ℝ) (↑r.den : ℝ) p ≠ 0
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p = HPow.hPow (α := ℝ) (↑r.den : ℝ) p * C / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p

Tactic:
simp [mul_rpow, mul_div_mul_left, this]

Premises used: Real.mul_rpow, mul_div_mul_left
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p (x + (↑r : ℝ))
⊢ LiouvilleWith p x

Tactic:
simpa using h.add_rat (-r)

Premises used: LiouvilleWith.add_rat, Neg.neg
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
r : ℚ
rw : LiouvilleWith p (x + (↑r : ℝ)) ↔ LiouvilleWith p x
rw₁ rw₂ : LiouvilleWith p x ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑r : ℝ) + x) ↔ LiouvilleWith p x

Tactic:
rw [add_comm, add_rat_iff]

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

Tactic:
add_comm x r ▸ h.add_rat r

Premises used: LiouvilleWith.add_rat, Eq.rec, Rat.cast, add_comm
-- 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 m, add_rat_iff]

Premises used: Rat.cast_intCast, LiouvilleWith.add_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 ((↑m : ℝ) + x) ↔ LiouvilleWith p x

Tactic:
rw [add_comm, add_int_iff]

Premises used: LiouvilleWith.add_int_iff, add_comm
-- 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 n, add_rat_iff]

Premises used: LiouvilleWith.add_rat_iff, Rat.cast_natCast
-- 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 ((↑n : ℝ) + x) ↔ LiouvilleWith p x

Tactic:
rw [add_comm, add_nat_iff]

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

Tactic:
add_int_iff.2 h

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

Tactic:
int_add_iff.2 h

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

Tactic:
h.add_int n

Premises used: LiouvilleWith.add_int, Nat.cast
-- Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
Goal:
p x : ℝ
h : LiouvilleWith p x
n : ℕ
⊢ LiouvilleWith p ((↑n : ℝ) + x)

Tactic:
h.int_add n

Premises used: LiouvilleWith.int_add, Nat.cast
-- 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),
    LiouvilleWith p (-x)
⊢ LiouvilleWith p (-x)

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
⊢ LiouvilleWith p (-x)

Tactic:
⟨C, hC.mono ?_⟩

Premises used: LiouvilleWith, Filter.Frequently.mono, Exists.intro