awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hT :
  ∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) + vonStaudtIndicator (2 * k) p =
    HMul.hMul (α := ℚ) (↑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 hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Fact.out : p.Prime).ne_zero
-- 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
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 : ℚ)
have 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)
Tactic: field_simp [hp_ne]
-- 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
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) * (↑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)
have 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
Tactic: linarith [hT, sum_pow_filter_eq_faulhaber p hk]
-- 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
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
⊢ 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)
have 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
Tactic: linarith [hT, sum_pow_filter_eq_faulhaber p hk]
-- 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
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
⊢ 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)
have 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
Tactic: linarith [hT, sum_pow_filter_eq_faulhaber p hk]
-- 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
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 : ℚ) =
    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 hAlg : 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]
-- 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
hT :
  ∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) + vonStaudtIndicator (2 * k) p =
    HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hAlg :
  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 : ℚ)
⊢ 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 : (↑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 : ℚ) =
  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: rw [hAlg]
-- 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
hT :
  ∑ v ∈ Ico 1 p, HPow.hPow (α := ℚ) (↑v : ℚ) (2 * k) + vonStaudtIndicator (2 * k) p =
    HMul.hMul (α := ℚ) (↑p : ℚ) (↑T : ℚ)
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hAlg :
  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 : ℚ)
⊢ (↑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 : ℚ) =
    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 : 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: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, ∀ (hk : m > 0), ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)).den
hk : k > 0
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den
have h : ∀ (T : ℤ)
  (hT :
    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))),
  ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den
Tactic: obtain ⟨T, hT⟩ := bernoulli_add_indicator_eq_sub (p := p) hk
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, ∀ (hk : m > 0), ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)).den
hk : k > 0
T : ℤ
hT :
  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))
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den
have h : ¬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))).den
Tactic: rw [hT]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, ∀ (hk : m > 0), ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)).den
hk : k > 0
T : ℤ
hT :
  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))
⊢ ¬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))).den
have hT_int : pIntegral p (↑T : ℚ)
Tactic: have hT_int : pIntegral p T := Int.padicValuation_le_one p T
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
k : ℕ
ih : ∀ m < k, ∀ (hk : m > 0), ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)).den
hk : k > 0
T : ℤ
hT :
  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))
hT_int : pIntegral p (↑T : ℚ)
⊢ ¬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))).den
have hR : pIntegral p
  (∑ i ∈ range (2 * k),
    bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
Tactic: have hR := pIntegral_faulhaber_sum hk fun m hm_pos hm_lt ↦
      Rat.padicValuation_le_one_iff.mpr (ih m hm_lt hm_pos)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den
have h : ∀ (k : ℕ) (ih : ∀ m < k, ∀ (hk : m > 0), ¬p ∣ (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)).den)
  (hk : k > 0), ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den
Tactic: induction k using Nat.strong_induction_on with
  | _ k ih =>
    obtain ⟨T, hT⟩ := bernoulli_add_indicator_eq_sub (p := p) hk
    rw [hT]
    have hT_int : pIntegral p T := Int.padicValuation_le_one p T
    have hR := pIntegral_faulhaber_sum hk fun m hm_pos hm_lt ↦
      Rat.padicValuation_le_one_iff.mpr (ih m hm_lt hm_pos)
    exact Rat.padicValuation_le_one_iff.mp ((Rat.padicValuation p).map_sub_le hT_int hR)
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ ¬p ∣ (bernoulli (2 * k) + ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den
have rw : ¬p ∣
    (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
        ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den
Tactic: rw [sum_one_div_prime_eq_indicator_div_add (p := p) hk, ← add_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ ¬p ∣
      (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
          ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den
have hcop_ind : (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den.Coprime p
Tactic: have hcop_ind := ((Nat.Prime.coprime_iff_not_dvd Fact.out).mpr
    (not_dvd_den_bernoulli_add_indicator (p := p) hk)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hcop_ind : (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den.Coprime p
⊢ ¬p ∣
      (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
          ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den
have hcop_rest : (Rat.den (∑ i ∈ vonStaudtPrimes k with i ≠ p, HDiv.hDiv (α := ℚ) 1 (↑i : ℚ))).Coprime p
Tactic: have hcop_rest := Nat.Coprime.of_dvd_left (Rat.den_sum_dvd_prod_den _ _)
    (prod_one_div_prime_den_coprime k (p := p))
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hcop_ind : (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den.Coprime p
hcop_rest : (Rat.den (∑ i ∈ vonStaudtPrimes k with i ≠ p, HDiv.hDiv (α := ℚ) 1 (↑i : ℚ))).Coprime p
⊢ ¬p ∣
      (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
          ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den
have hcop : p.Coprime
  (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
      ∑ i ∈ vonStaudtPrimes k with i ≠ p, HDiv.hDiv (α := ℚ) 1 (↑i : ℚ)).den
Tactic: have hcop := (Nat.Coprime.of_dvd_left (Rat.add_den_dvd _ _) (hcop_ind.mul_left hcop_rest)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k : ℕ
⊢ Membership.mem (γ := Set ℚ) (Set.range Int.cast)
    (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ))
have inl : Membership.mem (γ := Set ℚ) (Set.range Int.cast)
  (bernoulli (HMul.hMul (α := ℕ) 2 0) +
    ∑ p ∈ range (HMul.hMul (α := ℕ) 2 0 + 2) with Nat.Prime p ∧ p - 1 ∣ HMul.hMul (α := ℕ) 2 0,
      HDiv.hDiv (α := ℚ) 1 (↑p : ℚ))
Tactic: rcases Nat.eq_zero_or_pos k with rfl | hk
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k : ℕ
inl :
  Membership.mem (γ := Set ℚ) (Set.range Int.cast)
    (bernoulli (HMul.hMul (α := ℕ) 2 0) +
      ∑ p ∈ range (HMul.hMul (α := ℕ) 2 0 + 2) with Nat.Prime p ∧ p - 1 ∣ HMul.hMul (α := ℕ) 2 0,
        HDiv.hDiv (α := ℚ) 1 (↑p : ℚ))
⊢ Membership.mem (γ := Set ℚ) (Set.range Int.cast)
    (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ))
have inr : ∀ (hk : k > 0),
  Membership.mem (γ := Set ℚ) (Set.range Int.cast)
    (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ))
Tactic: rcases Nat.eq_zero_or_pos k with rfl | hk
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k : ℕ
hk : k > 0
⊢ ∃ (y : ℤ),
    (↑y : ℚ) =
      bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)
have inr : (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)).den = 1
Tactic: refine ⟨_, Rat.coe_int_num_of_den_eq_one ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k : ℕ
hk : k > 0
⊢ (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)).den = 1
have inr : ∀
  (h :
    ¬(bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)).den =
        1),
  False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k : ℕ
hk : k > 0
h :
  ¬(bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)).den = 1
⊢ False
have inr : ∀ (p : ℕ) (hp : Nat.Prime p)
  (hdvd :
    p ∣
      (bernoulli (2 * k) +
          ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)).den),
  False
Tactic: obtain ⟨p, hp, hdvd⟩ := ne_one_iff_exists_prime_dvd.mp h
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ bernoulli n = ∑ i ∈ range (n + 1), (monomial i : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - i) * (↑(n.choose i) : ℚ))
have rw : Eq (α := ℚ[X]) (∑ i ∈ range (n + 1), (monomial (n - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(n.choose i) : ℚ)))
  (∑ j ∈ range (n + 1),
    (monomial (n - j) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - j)) * (↑(n.choose (n - j)) : ℚ)))
Tactic: rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (goal)
Goal:
n : ℕ
⊢ Eq (α := ℚ[X]) (∑ i ∈ range (n + 1), (monomial (n - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(n.choose i) : ℚ)))
    (∑ j ∈ range (n + 1),
      (monomial (n - j) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - j)) * (↑(n.choose (n - j)) : ℚ)))
have apply : ∀ x ∈ range (n + 1),
  Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
    ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - x)) * (↑(n.choose (n - x)) : ℚ)) : ℚ[X])
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.BernoulliPolynomials (hypothesis)
Goal:
n x : ℕ
hx : x ∈ range (n + 1)
⊢ Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
    ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - (n - x)) * (↑(n.choose (n - x)) : ℚ)) : ℚ[X])
have hx₁ : x ≤ n
Tactic: rw [mem_range_succ_iff] at hx
Cleared hypotheses: hx