-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean
theorem partialSum_eq_rat {m : ℕ} (hm : 0 < m) (k : ℕ) :
    ∃ p : ℕ, partialSum m k = p / ((m ^ k ! :) : ℝ)

Proof state:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ 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:
simp [mul_assoc]

Result:
no goals

Proof state:
case succ
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (k + 1) = ↑p / ↑(m ^ (k + 1)!)

Tactic:
rcases h with ⟨p_k, h_k⟩

Result:
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (k + 1) = ↑p / ↑(m ^ (k + 1)!)

Proof state:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ partialSum (↑m) (k + 1) = ↑(p_k * m ^ ((k + 1)! - k !) + 1) / ↑(m ^ (k + 1)!)

Tactic:
rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]

Result:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑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)!)

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0

Proof state:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑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)!)

Tactic:
rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]

Result:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ 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 !)

Proof state:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑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)!)

Tactic:
norm_cast

Result:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑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)!)

Proof state:
case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0

Tactic:
all_goals positivity

Result:
no goals

Proof state:
m : ℕ
hm : 0 < m
⊢ partialSum (↑m) 0 = ↑1 / ↑(m ^ 0!)

Tactic:
rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
pow_one, pow_one]

Result:
no goals

Proof state:
case zero
m : ℕ
hm : 0 < m
⊢ ∃ p, partialSum (↑m) 0 = ↑p / ↑(m ^ 0!)

Tactic:
exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
pow_one, pow_one]⟩

Result:
no goals

Proof state:
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (k + 1) = ↑p / ↑(m ^ (k + 1)!)

Tactic:
use p_k * m ^ ((k + 1)! - k !) + 1

Result:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ partialSum (↑m) (k + 1) = ↑(p_k * m ^ ((k + 1)! - k !) + 1) / ↑(m ^ (k + 1)!)