awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have h : |x - HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
Tactic: refine ⟨⌊x * n⌋ + 1, this.ne, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ |x - HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
have h : HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ) < (x * (↑n : ℝ) + 2) / (↑n : ℝ)
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']
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ) < (x * (↑n : ℝ) + 2) / (↑n : ℝ)
have h : (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) < x * (↑n : ℝ) + 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) ≤ x * (↑n : ℝ) + 1
have push_cast : HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1 ≤ x * (↑n : ℝ) + 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1 ≤ x * (↑n : ℝ) + 1
have bc : (↑⌊x * (↑n : ℝ)⌋ : ℝ) ≤ x * (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ x * (↑n : ℝ) + 1 < x * (↑n : ℝ) + 2
have linarith : x * (↑n : ℝ) + 2 ≤ x * (↑n : ℝ) + 1 → -1 + (x * (↑n : ℝ) + 2 - (x * (↑n : ℝ) + 1)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
⊢ (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) < x * (↑n : ℝ) + 2
have calc : (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) ≤ x * (↑n : ℝ) + 1
Tactic: calc _ ≤ x * n + 1 := by push_cast; gcongr; apply Int.floor_le
    _ < x * n + 2 := by linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
⊢ (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) < x * (↑n : ℝ) + 2
have calc₁ : x * (↑n : ℝ) + 1 < x * (↑n : ℝ) + 2
Tactic: calc _ ≤ x * n + 1 := by push_cast; gcongr; apply Int.floor_le
    _ < x * n + 2 := by linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
⊢ ∃ (C : ℝ) (_ : 0 < C),
    ∃ᶠ (n : ℕ) in atTop,
      1 ≤ n ∧
        ∃ (m : ℤ),
          x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
            |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
have 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
Tactic: rcases h with ⟨C, hC⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have refine : ∃ᶠ (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 ⟨max C 1, zero_lt_one.trans_le <| le_max_right _ _, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have 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
Tactic: refine ((eventually_ge_atTop 1).and_frequently hC).mono ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have refine : C / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p
Tactic: refine ⟨hle, m, hne, hlt.trans_le ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ max C 1 / HPow.hPow (α := ℝ) (↑n : ℝ) p
have hab : C ≤ max C 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p q x : ℝ
h : LiouvilleWith p x
hle : q ≤ p
⊢ LiouvilleWith q x
have 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
Tactic: rcases h.exists_pos with ⟨C, hC₀, hC⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have 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
Tactic: refine ⟨C, hC.mono ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have refine : C / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ C / HPow.hPow (α := ℝ) (↑n : ℝ) q
Tactic: refine ⟨m, hne, hlt.trans_le <| ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
⊢ C / HPow.hPow (α := ℝ) (↑n : ℝ) p ≤ C / HPow.hPow (α := ℝ) (↑n : ℝ) q
have hdb : LE.le (α := ℝ) 1 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p q x : ℝ
h : LiouvilleWith p x
hlt : q < p
⊢ ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)
have 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)
Tactic: rcases h.exists_pos with ⟨C, _hC₀, hC⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)
have this : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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)
have 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)
Tactic: refine (this.and_frequently hC).mono ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (↑n : ℝ) (-q)
have hn₁ : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: replace hn : (0 : ℝ) < n := Nat.cast_pos.2 hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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)
have refine : C < HPow.hPow (α := ℝ) (↑n : ℝ) (-q) * HPow.hPow (α := ℝ) (↑n : ℝ) p
Tactic: refine ⟨m, hne, hlt.trans <| (div_lt_iff₀ <| rpow_pos_of_pos hn _).2 ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)
⊢ C < HPow.hPow (α := ℝ) (↑n : ℝ) (-q) * HPow.hPow (α := ℝ) (↑n : ℝ) p
have rwa : C < HPow.hPow (α := ℝ) (↑n : ℝ) p * HPow.hPow (α := ℝ) (↑n : ℝ) (-q)
Tactic: rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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)
⊢ C < HPow.hPow (α := ℝ) (↑n : ℝ) (-q) * HPow.hPow (α := ℝ) (↑n : ℝ) p
have rwa₁ : C < HPow.hPow (α := ℝ) (↑n : ℝ) (p + -q)
Tactic: rwa [mul_comm, ← rpow_add hn, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
⊢ LiouvilleWith p (x * (↑r : ℝ))
have 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 : ℝ))
Tactic: rcases h.exists_pos with ⟨C, _hC₀, hC⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ))
have 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
Tactic: refine ⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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
⊢ ∃ (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
have A : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have refine_1 : x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ)
Tactic: refine ⟨r.num * m, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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) : ℝ)
⊢ ∃ (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
have 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
Tactic: refine ⟨r.num * m, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ)
have refine_1 : x * (↑r : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) * (↑r : ℝ)
Tactic: rw [A]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 (α := ℝ) (↑(r.num * m) : ℝ) (↑(r.den • id n) : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
have refine_2 : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
  HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
Tactic: rw [A, ← sub_mul, abs_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
    HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HPow.hPow (α := ℝ) (↑(r.den • id n) : ℝ) p
have refine_2 : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| * |(↑r : ℝ)| <
  HPow.hPow (α := ℝ) (↑r.den : ℝ) p * ((↑|r| : ℝ) * C) / HMul.hMul (α := ℝ) (↑r.den : ℝ) (↑n : ℝ) ^ p
Tactic: simp only [smul_eq_mul, id, Nat.cast_mul]