-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hcast :
  Eq (α := ZMod p)
    (↑(HAdd.hAdd (α := ℤ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℤ) (↑v : ℤ) (2 * k)) (if p - 1 ∣ 2 * k then 1 else 0)) :
      ZMod p)
    0
T : ℤ
hT_int :
  HAdd.hAdd (α := ℤ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℤ) (↑v : ℤ) (2 * k)) (if p - 1 ∣ 2 * k then 1 else 0) =
    (↑p : ℤ) * T
hT :
  ∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) + vonStaudtIndicator (2 * k) p =
    HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
linarith linarith₁ linarith₂ :
  bernoulli (2 * k) * (↑p : ℚ) + vonStaudtIndicator (2 * k) p <
      HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ) -
        ∑ x ∈ range (2 * k),
          bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) →
    HMul.hMul (α := ℚ) 1 1 = 1
linarith₃ :
  bernoulli (2 * k) * (↑p : ℚ) + vonStaudtIndicator (2 * k) p <
      HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ) -
        ∑ x ∈ range (2 * k),
          bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) →
    -(∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) + vonStaudtIndicator (2 * k) p -
              HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ)) +
          (1 * bernoulli (2 * k) * HMul.hMul (α := ℚ) 1 (↑p : ℚ) + 1 * vonStaudtIndicator (2 * k) p -
            (HMul.hMul (α := ℚ) 1 (↑p : ℚ) * HMul.hMul (α := ℚ) 1 (↑T : ℚ) -
              HMul.hMul (α := ℚ) 1
                (∑ x ∈ range (2 * k),
                  bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
                    (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)))) +
        (HMul.hMul (α := ℚ) 1 (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) -
          (HMul.hMul (α := ℚ) 1
              (∑ i ∈ range (2 * k),
                bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
                  (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) +
            HMul.hMul (α := ℚ) 1 (↑p : ℚ) * (1 * bernoulli (2 * k)))) =
      0
linarith₄ linarith₅ linarith₆ :
  HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ) -
        ∑ x ∈ range (2 * k),
          bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) <
      bernoulli (2 * k) * (↑p : ℚ) + vonStaudtIndicator (2 * k) p →
    HMul.hMul (α := ℚ) 1 1 = 1
linarith₇ :
  HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ) -
        ∑ x ∈ range (2 * k),
          bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) <
      bernoulli (2 * k) * (↑p : ℚ) + vonStaudtIndicator (2 * k) p →
    ∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) + vonStaudtIndicator (2 * k) p -
            HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ) +
          (HMul.hMul (α := ℚ) 1 (↑p : ℚ) * HMul.hMul (α := ℚ) 1 (↑T : ℚ) -
              HMul.hMul (α := ℚ) 1
                (∑ x ∈ range (2 * k),
                  bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
                    (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) -
            (1 * bernoulli (2 * k) * HMul.hMul (α := ℚ) 1 (↑p : ℚ) + 1 * vonStaudtIndicator (2 * k) p)) +
        -(HMul.hMul (α := ℚ) 1 (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) -
            (HMul.hMul (α := ℚ) 1
                (∑ i ∈ range (2 * k),
                  bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
                    (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) +
              HMul.hMul (α := ℚ) 1 (↑p : ℚ) * (1 * bernoulli (2 * k)))) =
      0
⊢ bernoulli (2 * k) * (↑p : ℚ) + vonStaudtIndicator (2 * k) p =
    HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ) -
      ∑ x ∈ range (2 * k),
        bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)

Tactic:
linarith [hT, sum_pow_filter_eq_faulhaber p hk]

Premises used: _private.0.Bernoulli.sum_pow_filter_eq_faulhaber