awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
rw : LiouvilleWith p (x + (↑m : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑m : ℝ) + x) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [add_comm, add_int_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p (x + (↑n : ℝ)) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x + (↑(↑n : ℚ) : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_natCast n, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
rw : LiouvilleWith p (x + (↑(↑n : ℚ) : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x + (↑n : ℝ)) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_natCast n, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p ((↑n : ℝ) + x) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x + (↑n : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [add_comm, add_nat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
rw : LiouvilleWith p (x + (↑n : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p ((↑n : ℝ) + x) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [add_comm, add_nat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
h : LiouvilleWith p x
⊢ LiouvilleWith p (-x)
have 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)
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
⊢ LiouvilleWith p (-x)
have 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
Tactic: refine ⟨C, 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 : ℕ
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 : ℝ) p
have refine : |-x - HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
Tactic: refine ⟨-m, by simp [neg_div, hne], ?_⟩
-- 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 : ℕ
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
have h : |-x - HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ)| = |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
Tactic: convert! hlt using 1
-- 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 : ℕ
m : ℤ
hne : x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < C / HPow.hPow (α := ℝ) (↑n : ℝ) p
⊢ |-x - HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ)| = |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
have h : |HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ) - -x| = |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
Tactic: rw [abs_sub_comm]
-- 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 : ℕ
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 : ℝ)|
have h : HDiv.hDiv (α := ℝ) (↑(-m) : ℝ) (↑n : ℝ) - -x = x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
Tactic: congr! 1
-- 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 : ℕ
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 : ℝ)
have h : HDiv.hDiv (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ) - -x = x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p (x - (↑r : ℝ)) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x + -(↑r : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
rw : LiouvilleWith p (x + -(↑r : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x - (↑r : ℝ)) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p (x + (↑(-r) : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
r : ℚ
rw : LiouvilleWith p (x + -(↑r : ℝ)) ↔ LiouvilleWith p x
rw₁ : LiouvilleWith p (x + (↑(-r) : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x - (↑r : ℝ)) ↔ LiouvilleWith p x
have rw₂ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [sub_eq_add_neg, ← Rat.cast_neg, add_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x - (↑m : ℝ)) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x - (↑(↑m : ℚ) : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_intCast, sub_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
m : ℤ
rw : LiouvilleWith p (x - (↑(↑m : ℚ) : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x - (↑m : ℝ)) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_intCast, sub_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p (x - (↑n : ℝ)) ↔ LiouvilleWith p x
have rw : LiouvilleWith p (x - (↑(↑n : ℚ) : ℝ)) ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_natCast, sub_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p x : ℝ
n : ℕ
rw : LiouvilleWith p (x - (↑(↑n : ℚ) : ℝ)) ↔ LiouvilleWith p x
⊢ LiouvilleWith p (x - (↑n : ℝ)) ↔ LiouvilleWith p x
have rw₁ : LiouvilleWith p x ↔ LiouvilleWith p x
Tactic: rw [← Rat.cast_natCast, sub_rat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p (↑M : ℝ)
⊢ False
have rcases : ∀ (n : ℕ) (hn : 0 < n) (m : ℤ) (hne : (↑M : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ))
  (hlt : |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1)), 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 : ℝ)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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
have refine : HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) ≤ |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
Tactic: refine hlt.not_ge ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) ≤ |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
have hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: have hn' : (0 : ℝ) < n := by simpa
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)
⊢ HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) (-1) ≤ |(↑M : ℝ) - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)|
have rw : HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)| / (↑n : ℝ)
Tactic: rw [rpow_neg_one, ← one_div, sub_div' hn'.ne', abs_div, Nat.abs_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)
⊢ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)| / (↑n : ℝ)
have hab : 1 ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)
⊢ 1 ≤ |HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) - (↑m : ℝ)|
have hab : 1 ≤ |M * (↑n : ℤ) - m|
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)
⊢ 1 ≤ |M * (↑n : ℤ) - m|
have hab : M * (↑n : ℤ) ≠ m
Tactic: rw [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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 : ℝ)
⊢ M * (↑n : ℤ) ≠ m
have hne₁ : ¬HMul.hMul (α := ℝ) (↑M : ℝ) (↑n : ℝ) = (↑m : ℝ)
Tactic: rw [Ne, eq_div_iff hn'.ne'] at hne
Cleared hypotheses: hne, hlt, hn'
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
⊢ False
have inl : ∀ (h : LiouvilleWith p (↑0 : ℝ)), False
Tactic: rcases eq_or_ne r 0 with (rfl | h0)
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
inl : ∀ (h : LiouvilleWith p (↑0 : ℝ)), False
⊢ False
have inr : ∀ (h0 : r ≠ 0), False
Tactic: rcases eq_or_ne r 0 with (rfl | h0)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
h : LiouvilleWith p (↑0 : ℝ)
⊢ False
have inl : Eq (α := ℝ) (↑0 : ℝ) (↑0 : ℝ)
Tactic: refine h.ne_cast_int hp 0 ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
h : LiouvilleWith p (↑0 : ℝ)
⊢ Eq (α := ℝ) (↑0 : ℝ) (↑0 : ℝ)
have inl : Eq (α := ℝ) 0 (↑0 : ℝ)
Tactic: rw [Rat.cast_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
h : LiouvilleWith p (↑0 : ℝ)
inl : Eq (α := ℝ) 0 (↑0 : ℝ)
⊢ Eq (α := ℝ) (↑0 : ℝ) (↑0 : ℝ)
have inl₁ : Eq (α := ℝ) 0 0
Tactic: rw [Rat.cast_zero, Int.cast_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
⊢ False
have inr : HMul.hMul (α := ℝ) (↑r : ℝ) (↑r⁻¹ : ℝ) = (↑1 : ℝ)
Tactic: refine (h.mul_rat (inv_ne_zero h0)).ne_cast_int hp 1 ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
⊢ HMul.hMul (α := ℝ) (↑r : ℝ) (↑r⁻¹ : ℝ) = (↑1 : ℝ)
have inr : Eq (α := ℝ) 1 (↑1 : ℝ)
Tactic: rw [Rat.cast_inv, mul_inv_cancel₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p (↑r : ℝ)
h0 : r ≠ 0
inr : Eq (α := ℝ) 1 (↑1 : ℝ)
⊢ HMul.hMul (α := ℝ) (↑r : ℝ) (↑r⁻¹ : ℝ) = (↑1 : ℝ)
have inr₁ : Ne (α := ℝ) (↑r : ℝ) 0
Tactic: rw [Rat.cast_inv, mul_inv_cancel₀]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
hx : Liouville x
n : ℕ
⊢ ∃ᶠ (b : ℕ) in atTop,
    ∃ (a : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
have 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
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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 : ℝ)|
⊢ False
have H₁ : ∃ (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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)|
⊢ False
have rcases : ∀ (N : ℕ)
  (hN :
    ∀ b ≥ N,
      ∀ (a : ℤ) (_ : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)),
        1 / HPow.hPow (α := ℝ) (↑b : ℝ) n ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|),
  False
Tactic: rcases H with ⟨N, hN⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
have hb₁ : LT.lt (α := ℝ) 1 (↑b : ℝ)
Tactic: replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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)
have simp : Tendsto (β := ℝ) (fun (m : ℕ) ↦ (HPow.hPow (α := ℝ) (↑b : ℝ) m)⁻¹) atTop (𝓝 0)
Tactic: simp only [one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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 : ℝ)
⊢ ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
have H : 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)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)|
have refine : ∀ (x_1 : ℕ),
  (∀ (m : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ dist x (HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑b : ℝ))) →
    ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) x_1 ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
Tactic: refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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 : ℝ)|
⊢ False
have this : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
Tactic: have : ∀ b > (1 : ℕ), ∀ᶠ m : ℕ in atTop, ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| := by
    intro b hb
    replace hb : (1 : ℝ) < b := Nat.one_lt_cast.2 hb
    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)
    refine (H.eventually (hx.irrational.eventually_forall_le_dist_cast_div b)).mono ?_
    exact fun m hm a => hm a
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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 : ℝ)|
this :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
⊢ False
have this₁ : ∀ᶠ (m : ℕ) in atTop,
  ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
Tactic: have : ∀ᶠ m : ℕ in atTop, ∀ b < N, 1 < b → ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
    (finite_lt_nat N).eventually_all.2 fun b _hb => eventually_imp_distrib_left.2 (this b)
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
⊢ False
have rcases : ∀ (m : ℕ)
  (hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|)
  (hnm : n ≤ m), False
Tactic: rcases (this.and (eventually_ge_atTop n)).exists with ⟨m, hm, hnm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
⊢ False
have rcases : ∀ (a b : ℤ) (hb : 1 < b) (hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ))
  (hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m), False
Tactic: rcases hx m with ⟨a, b, hb, hne, hlt⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
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 : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a b : ℤ
hb : 1 < b
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m
⊢ False
have lift : ∀ (b : ℕ) (hb : LT.lt (α := ℤ) 1 (↑b : ℤ)) (hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ))
  (hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) m), False
Tactic: lift b to ℕ using zero_le_one.trans hb.le
Cleared hypotheses: b, hb, hne, hlt
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
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 : ℝ)|
this_1 :
  ∀ b > 1,
    ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
this :
  ∀ᶠ (m : ℕ) in atTop,
    ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
m : ℕ
hm : ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / HPow.hPow (α := ℝ) (↑b : ℝ) m ≤ |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)|
hnm : n ≤ m
a : ℤ
b : ℕ
hb : LT.lt (α := ℤ) 1 (↑b : ℤ)
hne : x ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)
hlt : |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) m
⊢ False
have hb₁ : 1 < b
Tactic: norm_cast at hb
Cleared hypotheses: hb