-- 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)!
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)

Tactic:
refine sum_congr rfl fun x _ => ?_

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 !
x : ℕ
x✝ : x ∈ range (p + 1)
⊢ bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) / ↑(p + 1)! * ↑p ! =
    bernoulli x * ↑((p + 1).choose x) * ↑n ^ (p + 1 - x) / (↑p + 1)

Proof state:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
⊢ ((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)!

Tactic:
ext q : 1

Result:
case h
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
⊢ (coeff ℚ q) ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    (coeff ℚ q)
      (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)!
this :
  (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)!
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
rw [PowerSeries.ext_iff] at this

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)!
this :
  ∀ (n_1 : ℕ),
    (coeff ℚ n_1) (PowerSeries.mk fun p => ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
      (coeff ℚ n_1)
        (PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ i ∈ range n, ↑i ^ p * (↑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)!
this :
  ∀ (n_1 : ℕ),
    (coeff ℚ n_1) (PowerSeries.mk fun p => ∑ k ∈ range n, ↑k ^ p * (algebraMap ℚ ℚ) (↑p !)⁻¹) =
      (coeff ℚ n_1)
        (PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!)
⊢ ∑ i ∈ range n, ↑i ^ p * (↑p !)⁻¹ =
    ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(p + 1)!

Tactic:
simpa using this p

Result:
no goals

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 < q + 1
⊢ bernoulli m * (↑(q + 1)! / (↑m ! * ↑(q + 1 - m)!)) * ↑n ^ (q + 1 - m) =
    bernoulli m * ↑q.succ ! / (↑m ! * ↑(q + 1 - m)!) * ↑n ^ (q + 1 - m)

Tactic:
ring

Result:
no goals

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

Tactic:
let f a b := bernoulli a / a ! * coeff ℚ (b + 1) (exp ℚ ^ n)

Result:
case h
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * (coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ (coeff ℚ q) ((PowerSeries.mk fun p => bernoulli p / ↑p !) * PowerSeries.mk fun q => (coeff ℚ (q + 1)) (exp ℚ ^ n)) =
    (coeff ℚ q)
      (PowerSeries.mk fun p => ∑ i ∈ range (p + 1), bernoulli i * ↑((p + 1).choose i) * ↑n ^ (p + 1 - i) / ↑(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))
        ({ 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)!

Tactic:
simp only [succ_eq_add_one, mem_range, f] at h

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 < q + 1
⊢ 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:
case h
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b => bernoulli a / ↑a ! * (coeff ℚ (b + 1)) (exp ℚ ^ n)
⊢ ∑ x ∈ range q.succ, bernoulli x / ↑x ! * (coeff ℚ (q - x + 1)) (exp ℚ ^ n) =
    ∑ i ∈ range (q + 1), bernoulli i * ↑((q + 1).choose i) * ↑n ^ (q + 1 - i) / ↑(q + 1)!

Tactic:
apply sum_congr rfl

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

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

Tactic:
intros m h

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)) (exp ℚ ^ n) =
    bernoulli m * ↑((q + 1).choose m) * ↑n ^ (q + 1 - m) / ↑(q + 1)!