-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
replace :
  Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
    (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
replace₁ :
  ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₂ :
  ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₃ :
  ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
replace₄ :
  ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0
replace₅ :
  ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0 =
    ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0
replace₆ :
  ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0 =
    ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0
replace₇ : ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0 = ∑ i ∈ range p.succ.succ, f' i
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ) (∑ i ∈ range p.succ.succ, f' i)

Tactic:
calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']

Premises used: Finset.Ico, Nat.cast, Finset.range, HPow.hPow, HAdd.hAdd, OfNat.ofNat, Nat.succ, Finset.sum