awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (hypothesis)
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h :
  ∀ (a : ℤ) (b : ℕ),
    1 ≤ HAdd.hAdd (α := ℝ) (↑b : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b : ℝ) 1| * A)
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a : ℤ
b : ℕ
b1 : LT.lt (α := ℤ) 1 (↑b : ℤ)
a1 :
  HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) r *
      (HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)|) <
    1
b0 : LT.lt (α := ℝ) 0 (↑(↑b : ℤ) : ℝ)
⊢ 1 / A ≤ HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)|
have h₁ : 1 ≤ HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1| * A)
Tactic: specialize h a b.pred
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.Basic (goal)
Goal:
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
r : ℕ
hn : A < HAdd.hAdd (α := ℝ) 1 1 ^ r
a : ℤ
b : ℕ
b1 : LT.lt (α := ℤ) 1 (↑b : ℤ)
a1 :
  HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) r *
      (HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)|) <
    1
b0 : LT.lt (α := ℝ) 0 (↑(↑b : ℤ) : ℝ)
h : 1 ≤ HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1 ^ f.natDegree * (|x - (↑a : ℝ) / HAdd.hAdd (α := ℝ) (↑b.pred : ℝ) 1| * A)
⊢ 1 / A ≤ HPow.hPow (α := ℝ) (↑(↑b : ℤ) : ℝ) f.natDegree * |x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑(↑b : ℤ) : ℝ)|
have rwa : ∀
  (h :
    1 ≤ HPow.hPow (α := ℝ) (↑b.pred.succ : ℝ) f.natDegree * (|x - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b.pred.succ : ℝ)| * A)),
  1 < b
Tactic: rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
      div_le_iff₀ hA] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
n : ℕ
m : ℝ
m1 : 1 < m
m0 : 0 < m
mi : 1 / m < 1
⊢ (∑' (i : ℕ), (1 / m) ^ i) * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
have rw : (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) = (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!)
Tactic: rw [tsum_geometric_of_lt_one (by positivity) mi]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!)
have hbc : (1 - 1 / m)⁻¹ ≤ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / (m ^ n !) ^ n
have rw : m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !
Tactic: rw [← pow_mul, div_le_div_iff₀, one_mul, mul_add_one, pow_add, mul_comm 2]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
rw : m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / (m ^ n !) ^ n
have hb : 0 < m ^ (n ! * (n + 1))
Tactic: rw [← pow_mul, div_le_div_iff₀, one_mul, mul_add_one, pow_add, mul_comm 2]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
rw : m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !
hb : 0 < m ^ (n ! * (n + 1))
⊢ 2 / m ^ (n ! * (n + 1)) ≤ 1 / (m ^ n !) ^ n
have hd : 0 < m ^ (n ! * n)
Tactic: rw [← pow_mul, div_le_div_iff₀, one_mul, mul_add_one, pow_add, mul_comm 2]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ m ^ (n ! * n) * 2 ≤ m ^ (n ! * n) * m ^ n !
have hbc : 2 ≤ m ^ n !
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
have rw : ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
Tactic: rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
rw :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! =
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
have rw₁ : ∑ i ∈ {0}, 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
Tactic: rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
rw :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! =
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₁ : ∑ i ∈ {0}, 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
have rw₂ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
Tactic: rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
rw :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! =
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₁ : ∑ i ∈ {0}, 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₂ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
have rw₃ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) 1 (↑(m ^ 0!) : ℝ)
Tactic: rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
rw :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! =
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₁ : ∑ i ∈ {0}, 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₂ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₃ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) 1 (↑(m ^ 0!) : ℝ)
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
have rw₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 1 = HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (β := ℕ) m 1) : ℝ)
Tactic: rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
rw :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! =
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₁ : ∑ i ∈ {0}, 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₂ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₃ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) 1 (↑(m ^ 0!) : ℝ)
rw₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 1 = HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (β := ℕ) m 1) : ℝ)
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
have rw₅ : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) = HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (β := ℕ) m 1) : ℝ)
Tactic: rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
rw :
  ∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1), 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! =
    HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₁ : ∑ i ∈ {0}, 1 / HPow.hPow (α := ℝ) (↑m : ℝ) i ! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₂ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
rw₃ : 1 / HPow.hPow (α := ℝ) (↑m : ℝ) 0! = HDiv.hDiv (α := ℝ) 1 (↑(m ^ 0!) : ℝ)
rw₄ : 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑m : ℝ) 1 = HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (β := ℕ) m 1) : ℝ)
rw₅ : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) = HDiv.hDiv (α := ℝ) 1 (↑(HPow.hPow (β := ℕ) m 1) : ℝ)
⊢ partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑1 : ℝ) (↑(m ^ 0!) : ℝ)
have rw₆ : HDiv.hDiv (α := ℝ) 1 (↑m : ℝ) = HDiv.hDiv (α := ℝ) 1 (↑m : ℝ)
Tactic: rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ (p : ℕ), partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ k !) : ℝ)
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)
have succ : ∀ (p_k : ℕ) (h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)),
  ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)
Tactic: rcases h with ⟨p_k, h_k⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)
have h : partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)
Tactic: use p_k * m ^ ((k + 1)! - k !) + 1
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)
have h : (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
    HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
  (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)
Tactic: rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h :
  (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
      HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
    (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)
⊢ partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)
have h₁ : (↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0
Tactic: rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h :
  (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
      HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
    (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)
h₁ : (↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0
⊢ partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)
have h₂ : Ne (α := ℝ) (↑(m ^ (k + 1)!) : ℝ) 0
Tactic: rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h :
  (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
      HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
    (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)
h₁ : (↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0
h₂ : Ne (α := ℝ) (↑(m ^ (k + 1)!) : ℝ) 0
⊢ partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)
have h₃ : Ne (α := ℝ) (↑(m ^ k !) : ℝ) 0
Tactic: rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
h :
  (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
      HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
    (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)
h₁ : (↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0
h₂ : Ne (α := ℝ) (↑(m ^ (k + 1)!) : ℝ) 0
h₃ : Ne (α := ℝ) (↑(m ^ k !) : ℝ) 0
⊢ partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) (↑(m ^ (k + 1)!) : ℝ)
have h₄ : HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! ≠ 0
Tactic: rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ (↑p_k : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)! * (↑(m ^ (k + 1)!) : ℝ) +
      HMul.hMul (α := ℝ) (↑(m ^ k !) : ℝ) 1 * (↑(m ^ (k + 1)!) : ℝ) =
    (↑(p_k * m ^ ((k + 1)! - k !) + 1) : ℝ) * ((↑(m ^ k !) : ℝ) * HPow.hPow (α := ℝ) (↑m : ℝ) (k + 1)!)
have h : p_k * m ^ (k + 1)! * m ^ (k + 1)! + m ^ k ! * 1 * m ^ (k + 1)! =
  (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p_k : ℝ) (↑(m ^ k !) : ℝ)
⊢ p_k * m ^ (k + 1)! * m ^ (k + 1)! + m ^ k ! * 1 * m ^ (k + 1)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)
have h : p_k * (m ^ (k * k !) * m ^ k !) * (m ^ (k * k !) * m ^ k !) + m ^ k ! * 1 * (m ^ (k * k !) * m ^ k !) =
  p_k * m ^ (k * k !) * (m ^ k ! * (m ^ (k * k !) * m ^ k !)) + m ^ k ! * (m ^ (k * k !) * m ^ k !)
Tactic: rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k : ℕ
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ k !) : ℝ)
have zero : ∃ (p : ℕ), partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ 0!) : ℝ)
Tactic: induction k with
  | zero => exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]⟩
  | succ k h =>
    rcases h with ⟨p_k, h_k⟩
    use p_k * m ^ ((k + 1)! - k !) + 1
    rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
    · norm_cast
      rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
      simp [mul_assoc]
    all_goals positivity
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 0 < m
k : ℕ
zero : ∃ (p : ℕ), partialSum (↑m : ℝ) 0 = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ 0!) : ℝ)
⊢ ∃ (p : ℕ), partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ k !) : ℝ)
have succ : ∀ (k : ℕ) (h : ∃ (p : ℕ), partialSum (↑m : ℝ) k = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ k !) : ℝ)),
  ∃ (p : ℕ), partialSum (↑m : ℝ) (k + 1) = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ (k + 1)!) : ℝ)
Tactic: induction k with
  | zero => exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]⟩
  | succ k h =>
    rcases h with ⟨p_k, h_k⟩
    use p_k * m ^ ((k + 1)! - k !) + 1
    rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
    · norm_cast
      rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
      simp [mul_assoc]
    all_goals positivity
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 2 ≤ m
⊢ LT.lt (α := ℤ) 1 (↑m : ℤ)
have norm_cast : 1 < m
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (hypothesis)
Goal:
m : ℕ
hm : 2 ≤ m
⊢ Liouville (liouvilleNumber (↑m : ℝ))
have mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
Tactic: have mZ1 : 1 < (m : ℤ) := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
⊢ LT.lt (α := ℝ) 1 (↑m : ℝ)
have norm_cast : 1 < m
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (hypothesis)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
⊢ Liouville (liouvilleNumber (↑m : ℝ))
have m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
Tactic: have m1 : 1 < (m : ℝ) := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n : ℕ
⊢ ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
have rcases : ∀ (p : ℕ) (hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)),
  ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
Tactic: rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)
⊢ ∃ (a : ℤ) (b : ℤ),
    1 < b ∧
      liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ) ∧
        |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑a : ℝ) (↑b : ℝ)| < 1 / HPow.hPow (α := ℝ) (↑b : ℝ) n
have refine : liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) ∧
  |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ)| <
    1 / HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) n
Tactic: refine ⟨p, m ^ n !, one_lt_pow₀ mZ1 n.factorial_ne_zero, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)
⊢ liouvilleNumber (↑m : ℝ) ≠ HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) ∧
    |liouvilleNumber (↑m : ℝ) - HDiv.hDiv (α := ℝ) (↑(↑p : ℤ) : ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ)| <
      1 / HPow.hPow (α := ℝ) (↑(HPow.hPow (α := ℤ) (↑m : ℤ) n !) : ℝ) n
have push_cast : liouvilleNumber (↑m : ℝ) ≠ (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ∧
  |liouvilleNumber (↑m : ℝ) - (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (hypothesis)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ)
⊢ liouvilleNumber (↑m : ℝ) ≠ (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ∧
    |liouvilleNumber (↑m : ℝ) - (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n
have hp₁ : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
Tactic: rw [Nat.cast_pow] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
⊢ liouvilleNumber (↑m : ℝ) ≠ (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ∧
    |liouvilleNumber (↑m : ℝ) - (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n
have rw : partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n ≠ partialSum (↑m : ℝ) n ∧
  |partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n - partialSum (↑m : ℝ) n| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n
Tactic: rw [← partialSum_add_remainder m1 n, ← hp]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (hypothesis)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
⊢ partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n ≠ partialSum (↑m : ℝ) n ∧
    |partialSum (↑m : ℝ) n + remainder (↑m : ℝ) n - partialSum (↑m : ℝ) n| < 1 / HPow.hPow (α := ℝ) (↑m : ℝ) n ! ^ n
have hpos : 0 < remainder (↑m : ℝ) n
Tactic: have hpos := remainder_pos m1 n
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber (goal)
Goal:
m : ℕ
hm : 2 ≤ m
mZ1 : LT.lt (α := ℤ) 1 (↑m : ℤ)
m1 : LT.lt (α := ℝ) 1 (↑m : ℝ)
n p : ℕ
hp : partialSum (↑m : ℝ) n = (↑p : ℝ) / HPow.hPow (α := ℝ) (↑m : ℝ) n !
hpos : 0 < remainder (↑m : ℝ) n
⊢ LE.le (α := ℝ) 2 (↑m : ℝ)
have assumption_mod_cast : ∀ (mZ1 m1 : 1 < m) (hp : partialSum (↑m : ℝ) n = HDiv.hDiv (α := ℝ) (↑p : ℝ) (↑(m ^ n !) : ℝ))
  (hpos : 0 < remainder (↑m : ℝ) n), 2 ≤ m
Tactic: assumption_mod_cast
Cleared hypotheses: mZ1, m1, hp, hpos
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
⊢ LiouvilleWith 1 x
have h : ∃ᶠ (n : ℕ) in atTop,
  ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
Tactic: use 2
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (goal)
Goal:
x : ℝ
⊢ ∃ᶠ (n : ℕ) in atTop,
    ∃ (m : ℤ),
      x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
        |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
have h : ∀ (n : ℕ) (hn : 0 < n),
  ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
Tactic: refine ((eventually_gt_atTop 0).mono fun n hn => ?_).frequently
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
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:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
have rw : x * (↑n : ℝ) < HAdd.hAdd (α := ℝ) (↑⌊x * (↑n : ℝ)⌋ : ℝ) 1
Tactic: rw [lt_div_iff₀ hn', Int.cast_add, Int.cast_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith (hypothesis)
Goal:
x : ℝ
n : ℕ
hn : 0 < n
hn' : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∃ (m : ℤ),
    x ≠ HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ∧
      |x - HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)| < 2 / HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1
have this : x < HDiv.hDiv (α := ℝ) (↑(⌊x * (↑n : ℝ)⌋ + 1) : ℝ) (↑n : ℝ)
Tactic: have : x < ↑(⌊x * ↑n⌋ + 1) / ↑n := by
    rw [lt_div_iff₀ hn', Int.cast_add, Int.cast_one]
    exact Int.lt_floor_add_one _