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

case succ
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
m : ℕ
hm : 0 < m
k : ℕ
⊢ ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
induction' k with k h
no goals
case zero
m : ℕ
hm : 0 < m
⊢ ∃ p, partialSum (↑m) Nat.zero = ↑p / ↑(m ^ Nat.zero !)
exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
  pow_one, pow_one]⟩
no goals
m : ℕ
hm : 0 < m
⊢ partialSum (↑m) Nat.zero = ↑1 / ↑(m ^ Nat.zero !)
rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
pow_one, pow_one]
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
case succ
m : ℕ
hm : 0 < m
k : ℕ
h : ∃ p, partialSum (↑m) k = ↑p / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
rcases h with ⟨p_k, h_k⟩
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ partialSum (↑m) (Nat.succ k) = ↑(p_k * m ^ ((k + 1)! - k !) + 1) / ↑(m ^ (Nat.succ k)!)
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ∃ p, partialSum (↑m) (Nat.succ k) = ↑p / ↑(m ^ (Nat.succ k)!)
use p_k * m ^ ((k + 1)! - k !) + 1
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (Nat.succ k)!) + ↑(m ^ k !) * 1 * ↑(m ^ (Nat.succ k)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)

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

case succ.intro.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (Nat.succ k)!) ≠ 0

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

case succ.intro.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ partialSum (↑m) (Nat.succ k) = ↑(p_k * m ^ ((k + 1)! - k !) + 1) / ↑(m ^ (Nat.succ k)!)
rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
no goals
case succ.intro.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

case succ.intro.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (Nat.succ k)!) ≠ 0

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

case succ.intro.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
all_goals positivity
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k + 1)! * m ^ (Nat.succ k)! + m ^ k ! * 1 * m ^ (Nat.succ k)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (Nat.succ k)!) + ↑(m ^ k !) * 1 * ↑(m ^ (Nat.succ k)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)
norm_cast
case succ.intro
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 !)
case succ.intro
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k + 1)! * m ^ (Nat.succ k)! + m ^ k ! * 1 * m ^ (Nat.succ k)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)
rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
no goals
case succ.intro
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 !)
simp [mul_assoc]
no goals
case succ.intro.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
positivity