awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
hi : HAdd.hAdd (α := ℕ) 0 1 < 2 * k
hp2 : p ≠ 2
⊢ 2 < p

Tactic:
exact (Prime.odd_iff Fact.out).mp <| Prime.odd_of_ne_two Fact.out hp2

Premises used: Nat.Prime.odd_of_ne_two, Iff.mp, Nat.Prime.odd_iff, Fact.out
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
succ :
  ∀ (m : ℕ) (hm : i + 2 = m + m),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
          (bernoulli (i + 1 + 1) * (↑((2 * k + 1).choose (i + 1 + 1)) : ℚ) *
              HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - (i + 1 + 1)) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
succ₁ :
  ∀ (hodd : Odd (i + 2)),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
          (bernoulli (i + 1 + 1) * (↑((2 * k + 1).choose (i + 1 + 1)) : ℚ) *
              HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - (i + 1 + 1)) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli (i + 1 + 1) * (↑((2 * k + 1).choose (i + 1 + 1)) : ℚ) *
            HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - (i + 1 + 1)) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rcases Nat.even_or_odd (i + 2) with ⟨m, hm⟩ | hodd

Premises used: HAdd.hAdd, OfNat.ofNat, Nat.even_or_odd
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
⊢ 0 < m ∧ m < k ∧ i + 2 = 2 * m

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
⊢ 0 < m

Tactic:
have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
hm_pos : 0 < m
⊢ m < k

Tactic:
have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
hm_pos : 0 < m
hm_lt : m < k
⊢ i + 2 = 2 * m

Tactic:
have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
hm_pos : 0 < m
hm_lt : m < k
hi_eq : i + 2 = 2 * m
succ :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli (i + 1 + 1) * (↑((2 * k + 1).choose (i + 1 + 1)) : ℚ) *
            HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - (i + 1 + 1)) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp only [hi_eq]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
hm_pos : 0 < m
hm_lt : m < k
hi_eq : i + 2 = 2 * m
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
pIntegral_bernoulli_even_term hm_lt (ih m hm_pos hm_lt)

Premises used: _private.0.Bernoulli.pIntegral_bernoulli_even_term
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
m : ℕ
hm : i + 2 = m + m
hm_pos : 0 < m
hm_lt : m < k
hi_eq : i + 2 = 2 * m
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
exact pIntegral_bernoulli_even_term hm_lt (ih m hm_pos hm_lt)

Premises used: _private.0.Bernoulli.pIntegral_bernoulli_even_term
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
hodd : Odd (i + 2)
⊢ 1 < i + 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
i : ℕ
hi : i + 1 + 1 < 2 * k
hodd : Odd (i + 2)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli (i + 1 + 1) * (↑((2 * k + 1).choose (i + 1 + 1)) : ℚ) *
            HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - (i + 1 + 1)) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp [bernoulli_eq_zero_of_odd hodd (by lia)]

Premises used: bernoulli_eq_zero_of_odd
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : 0 < k
zero :
  Eq (α := ℚ) (∑ v ∈ Ico 1 0, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range 0, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
succ :
  ∀ (n : ℕ),
    Eq (α := ℚ) (∑ v ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
      (∑ v ∈ range (n + 1), HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
⊢ Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))

Tactic:
cases p
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k : ℕ
hk : 0 < k
⊢ 2 * k ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k : ℕ
hk : 0 < k
⊢ Eq (α := ℚ) (∑ v ∈ Ico 1 0, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range 0, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))

Tactic:
simp [Finset.sum_range_eq_add_Ico, show 2 * k ≠ 0 by lia]

Premises used: Finset.sum_range_eq_add_Ico
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k : ℕ
hk : 0 < k
n : ℕ
⊢ 2 * k ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k : ℕ
hk : 0 < k
n : ℕ
⊢ Eq (α := ℚ) (∑ v ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
    (∑ v ∈ range (n + 1), HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))

Tactic:
simp [Finset.sum_range_eq_add_Ico, show 2 * k ≠ 0 by lia]

Premises used: Finset.sum_range_eq_add_Ico
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : 0 < k
⊢ Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))

Tactic:
have hfilter : (∑ v ∈ Ico 1 p, (v : ℚ) ^ (2 * k)) = ∑ v ∈ range p, (v : ℚ) ^ (2 * k) := by
    cases p <;> simp [Finset.sum_range_eq_add_Ico, show 2 * k ≠ 0 by lia]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : 0 < k
hfilter :
  Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
⊢ 2 * k + 1 - 2 * k = 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : 0 < k
hfilter :
  Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
rw :
  ∑ x ∈ range (2 * k),
        bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
          HAdd.hAdd (α := ℚ) (↑(2 * k) : ℚ) 1 +
      bernoulli (2 * k) * (↑(2 * k + 1) : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑p : ℚ) 1 /
        HAdd.hAdd (α := ℚ) (↑(2 * k) : ℚ) 1 =
    ∑ i ∈ range (2 * k),
        bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) +
      (↑p : ℚ) * bernoulli (2 * k)
⊢ ∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) =
    ∑ i ∈ range (2 * k),
        bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) +
      (↑p : ℚ) * bernoulli (2 * k)

Tactic:
rw [hfilter, sum_range_pow, Finset.sum_range_succ, Nat.choose_succ_self_right,
    show 2 * k + 1 - 2 * k = 1 by lia]

Premises used: Nat.choose_succ_self_right, sum_range_pow, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : 0 < k
hfilter :
  Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
push_cast :
  ∑ 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) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * HPow.hPow (α := ℚ) (β := ℕ) (↑p : ℚ) 1 /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    ∑ i ∈ range (2 * k),
        bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) +
      (↑p : ℚ) * bernoulli (2 * k)
⊢ ∑ x ∈ range (2 * k),
        bernoulli x * (↑((2 * k + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - x) /
          HAdd.hAdd (α := ℚ) (↑(2 * k) : ℚ) 1 +
      bernoulli (2 * k) * (↑(2 * k + 1) : ℚ) * HPow.hPow (α := ℚ) (β := ℕ) (↑p : ℚ) 1 /
        HAdd.hAdd (α := ℚ) (↑(2 * k) : ℚ) 1 =
    ∑ i ∈ range (2 * k),
        bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) +
      (↑p : ℚ) * bernoulli (2 * k)

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : 0 < k
hfilter :
  Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
⊢ ∑ 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) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * HPow.hPow (α := ℚ) (β := ℕ) (↑p : ℚ) 1 /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    ∑ i ∈ range (2 * k),
        bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) +
      (↑p : ℚ) * bernoulli (2 * k)

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Fact.out : p.Prime).ne_zero
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
rw :
  Eq (α := ℚ)
    (∑ i ∈ range (2 * k),
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) /
        (↑p : ℚ))
    (∑ i ∈ range (2 * k),
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
⊢ HDiv.hDiv (α := ℚ)
      (∑ i ∈ range (2 * k),
        bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
      (↑p : ℚ) =
    ∑ i ∈ range (2 * k),
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)

Tactic:
rw [Finset.sum_div]

Premises used: Finset.sum_div
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
⊢ Eq (α := ℚ)
    (∑ i ∈ range (2 * k),
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) /
        (↑p : ℚ))
    (∑ i ∈ range (2 * k),
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))

Tactic:
Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
refine :
  ∀ (i : ℕ) (hi : i ∈ range (2 * k)),
    bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) /
        (↑p : ℚ) =
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
⊢ Eq (α := ℚ)
    (∑ i ∈ range (2 * k),
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) /
        (↑p : ℚ))
    (∑ i ∈ range (2 * k),
      bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))

Tactic:
refine Finset.sum_congr rfl fun i hi ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
i : ℕ
hi : i ∈ range (2 * k)
⊢ i < 2 * k

Tactic:
have := Finset.mem_range.mp hi
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ 2 * k + 1 - i = 2 * k - i + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
rw :
  bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) * (↑p : ℚ)) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) /
      (↑p : ℚ) =
    bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
⊢ bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) /
      (↑p : ℚ) =
    bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)

Tactic:
rw [show 2 * k + 1 - i = (2 * k - i) + 1 by lia, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
i : ℕ
hi : i ∈ range (2 * k)
this : i < 2 * k
⊢ bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) * (↑p : ℚ)) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) /
      (↑p : ℚ) =
    bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)

Tactic:
field_simp [hp_ne]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ 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

Tactic:
have hcast : (↑((∑ v ∈ Ico 1 p, (v : ℤ) ^ (2 * k)) +
      (if (p - 1) ∣ 2 * k then 1 else 0)) : ZMod p) = 0 :=
    mod_cast sum_pow_add_indicator_eq_zero (p := p) _
-- 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
obtain :
  ∀ (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),
    ∃ (T : ℤ),
      bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) =
        HSub.hSub (α := ℚ) (↑T : ℚ)
          (∑ i ∈ range (2 * k),
            bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
              (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
⊢ ∃ (T : ℤ),
    bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) =
      HSub.hSub (α := ℚ) (↑T : ℚ)
        (∑ i ∈ range (2 * k),
          bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))

Tactic:
obtain ⟨T, hT_int⟩ := (ZMod.intCast_zmod_eq_zero_iff_dvd _ _).mp hcast

Premises used: ZMod.intCast_zmod_eq_zero_iff_dvd, Iff.mp
-- 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
h :
  bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) =
    HSub.hSub (α := ℚ) (↑T : ℚ)
      (∑ i ∈ range (2 * k),
        bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
⊢ ∃ (T : ℤ),
    bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) =
      HSub.hSub (α := ℚ) (↑T : ℚ)
        (∑ i ∈ range (2 * k),
          bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))

Tactic:
use T
-- 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
⊢ HAdd.hAdd (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (if p - 1 ∣ 2 * k then 1 else 0) =
    HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ)

Tactic:
exact_mod_cast hT_int
-- 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
⊢ ∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) + vonStaudtIndicator (2 * k) p =
    HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ)

Tactic:
have hT : (∑ v ∈ Ico 1 p, (v : ℚ) ^ (2 * k)) + vonStaudtIndicator (2 * k) p =
      p * T := by unfold vonStaudtIndicator; exact_mod_cast hT_int
-- 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 : ℚ)
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero
-- 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
field_simp :
  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)
⊢ bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) =
    (↑T : ℚ) -
      HDiv.hDiv (α := ℚ)
        (∑ i ∈ range (2 * k),
          bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
        (↑p : ℚ)

Tactic:
field_simp [hp_ne]
-- 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
⊢ bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) =
    (↑T : ℚ) -
      HDiv.hDiv (α := ℚ)
        (∑ i ∈ range (2 * k),
          bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k + 1 - i) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
        (↑p : ℚ)

Tactic:
have hAlg : bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / p =
      T - (∑ i ∈ range (2 * k), bernoulli i * ((2 * k + 1).choose i) *
        (p : ℚ) ^ (2 * k + 1 - i) / (2 * k + 1)) / p := by
    field_simp [hp_ne]; linarith [hT, sum_pow_filter_eq_faulhaber p hk]