-- Mathlib/NumberTheory/Bernoulli.lean
theorem sum_range_pow (n p : ℕ) :
    (∑ k ∈ range n, (k : ℚ) ^ p) =
      ∑ i ∈ range (p + 1), bernoulli i * ((p + 1).choose i) * (n : ℚ) ^ (p + 1 - i) / (p + 1)

Proof state:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ (PowerSeries.mk fun p => ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
have hexp : exp ℚ - 1 ≠ 0 := by
  simp only [exp, PowerSeries.ext_iff, Ne, not_forall]
  use 1
  simp [factorial_ne_zero]

Result:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
⊢ (PowerSeries.mk fun p => ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Proof state:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_const : (C ℚ) ((constantCoeff ℚ) (exp ℚ ^ n)) = 1
⊢ exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => (coeff ℚ (p + 1)) (exp ℚ ^ n)

Tactic:
rw [← h_const, sub_const_eq_X_mul_shift]

Result:
no goals

Proof state:
n p : ℕ
⊢ ∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Tactic:
have hne : ∀ m : ℕ, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m

Result:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ ∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Proof state:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
⊢ (C ℚ) ((constantCoeff ℚ) (exp ℚ ^ n)) = 1

Tactic:
simp

Result:
no goals

Proof state:
case h.hn
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * (coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m < q + 1
⊢ ↑(m ! * (q + 1 - m)!) ≠ 0

Tactic:
simp [hne, factorial_ne_zero]

Result:
no goals

Proof state:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !

Tactic:
suffices
  (mk fun p => ∑ k ∈ range n, (k : ℚ) ^ p * algebraMap ℚ ℚ p !⁻¹) =
    mk fun p =>
      ∑ i ∈ range (p + 1), bernoulli i * (p + 1).choose i * (n : ℚ) ^ (p + 1 - i) / (p + 1)! by
  rw [← div_eq_iff (hne p), div_eq_mul_inv, sum_mul]
  rw [PowerSeries.ext_iff] at this
  simpa using this p

Result:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
⊢ (PowerSeries.mk fun p => ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Proof state:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => (coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n => (algebraMap ℚ ℚ) (bernoulli n / ↑n !)) *
        PowerSeries.mk fun p => (coeff ℚ (p + 1)) (exp ℚ ^ n)) *
      (exp ℚ - 1) =
    (exp ℚ - 1) *
      PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
simp only [mul_comm, mul_eq_mul_left_iff, hexp, or_false]

Result:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hexp : exp ℚ - 1 ≠ 0
h_r : exp ℚ ^ n - 1 = X * PowerSeries.mk fun p => (coeff ℚ (p + 1)) (exp ℚ ^ n)
⊢ ((PowerSeries.mk fun n => (algebraMap ℚ ℚ) (bernoulli n / ↑n !)) *
      PowerSeries.mk fun p => (coeff ℚ (p + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ x ∈ range (p + 1), ↑n ^ (p + 1 - x) * (bernoulli x * ↑((p + 1).choose x)) / ↑(p + 1)!

Proof state:
case h
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * (coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range q.succ
⊢ bernoulli m / ↑m ! * (coeff ℚ (q - m + 1)) (exp ℚ ^ n) =
    bernoulli m * ↑((q + 1).choose m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!

Tactic:
simp only [f, exp_pow_eq_rescale_exp, rescale, one_div, coeff_mk, RingHom.coe_mk, coeff_exp,
  RingHom.id_apply, cast_mul, Algebra.id.map_eq_id]

Result:
case h
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * (coeff ℚ (b + 1)) (exp ℚ ^ n)
m : ℕ
h : m ∈ range q.succ
⊢ bernoulli m / ↑m ! *
      (coeff ℚ (q - m + 1))
        ({ toFun := fun f => PowerSeries.mk fun n_1 => ↑n ^ n_1 * (coeff ℚ n_1) f, map_one' := ⋯, map_mul' := ⋯ }
          (exp ℚ)) =
    bernoulli m * ↑((q + 1).choose m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!

Proof state:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ ∑ k ∈ range n, ↑k ^ p = ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)

Tactic:
rw [hps, sum_mul]

Result:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
h_cauchy :
  ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!
hps :
  ∑ k ∈ range n, ↑k ^ p = (∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!) * ↑p !
⊢ ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)! * ↑p ! =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / (↑p + 1)