awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (-1 / 2 * (↑(2 * k + 1) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have succ : LE.le (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
      (-1 / 2 * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (-1 / 2 * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have succ : LE.le (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2)) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have succ : ∀ [inst : Fact (Nat.Prime 2)]
  (ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral 2 (bernoulli (2 * m) + vonStaudtIndicator (2 * m) 2 / (↑2 : ℚ))),
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation 2 : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑2 : ℚ) (2 * k - 1) / 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
Tactic: obtain rfl | hp2 := eq_or_ne p 2
Cleared hypotheses: p, inst, ih
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
succ :
  ∀ [inst : Fact (Nat.Prime 2)]
    (ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral 2 (bernoulli (2 * m) + vonStaudtIndicator (2 * m) 2 / (↑2 : ℚ))),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation 2 : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑2 : ℚ) (2 * k - 1) / 2)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have succ₁ : ∀ (hp2 : p ≠ 2),
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
Tactic: obtain rfl | hp2 := eq_or_ne p 2
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k : ℕ
hk : k > 0
hi : HAdd.hAdd (α := ℕ) 0 1 < 2 * k
inst : Fact (Nat.Prime 2)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral 2 (bernoulli (2 * m) + vonStaudtIndicator (2 * m) 2 / (↑2 : ℚ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation 2 : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) 2 (2 * k - 1) / 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have succ : LE.le (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation 2 : (a : ℚ) → WithZero (Multiplicative ℤ)) (-HPow.hPow (α := ℚ) 2 (2 * k - 2)) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [show 2 * k - 1 = (2 * k - 2) + 1 by lia, pow_succ, mul_div_cancel_right₀ _ two_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have succ : LE.le (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [Valuation.map_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have succ : 2 < p
Tactic: refine pIntegral_pow_div two_ne_zero <|
         (factorization_eq_zero_of_lt ?_).trans_le (by lia)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ 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 ℤ))
have 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 ℤ))
Tactic: rcases Nat.even_or_odd (i + 2) with ⟨m, hm⟩ | hodd
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
Tactic: rcases Nat.even_or_odd (i + 2) with ⟨m, hm⟩ | hodd
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ 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 ℤ))
have hm_pos : 0 < m
Tactic: have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ 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 ℤ))
have hm_lt : m < k
Tactic: have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ 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 ℤ))
have hi_eq : i + 2 = 2 * m
Tactic: have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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 (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 ℤ))
have 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 ℤ))
Tactic: simp only [hi_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : 0 < k
⊢ Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
have zero : Eq (α := ℚ) (∑ v ∈ Ico 1 0, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range 0, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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))
⊢ Eq (α := ℚ) (∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k)) (∑ v ∈ range p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
have succ : ∀ (n : ℕ),
  Eq (α := ℚ) (∑ v ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
    (∑ v ∈ range (n + 1), HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k))
Tactic: cases p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
hk : 0 < 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)
have hfilter : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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))
⊢ ∑ 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)
have 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)
Tactic: rw [hfilter, sum_range_pow, Finset.sum_range_succ, Nat.choose_succ_self_right,
    show 2 * k + 1 - 2 * k = 1 by lia]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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) /
          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)
have 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)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
⊢ 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)
have hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Fact.out : p.Prime).ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
⊢ 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)
have 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))
Tactic: rw [Finset.sum_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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))
have 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)
Tactic: refine Finset.sum_congr rfl fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
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)
have this : i < 2 * k
Tactic: have := Finset.mem_range.mp hi
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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 + 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)
have 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)
Tactic: rw [show 2 * k + 1 - i = (2 * k - i) + 1 by lia, pow_succ]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ ∃ (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))
have 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
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) _
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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 : ℤ),
    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))
have 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))
Tactic: obtain ⟨T, hT_int⟩ := (ZMod.intCast_zmod_eq_zero_iff_dvd _ _).mp hcast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ ∃ (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))
have 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))
Tactic: use T
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ 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))
have hT : ∑ 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