awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 : ℚ)
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))
⊢ 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:
rw [hAlg]
-- 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
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 : ℚ)
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)
⊢ (↑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:
congr 1
-- 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
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 : ℚ)
⊢ 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:
simpa using faulhaber_sum_div_prime_eq

Premises used: _private.0.Bernoulli.faulhaber_sum_div_prime_eq
-- Module: Mathlib.NumberTheory.Bernoulli
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
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
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den

Tactic:
obtain ⟨T, hT⟩ := bernoulli_add_indicator_eq_sub (p := p) hk

Premises used: _private.0.Bernoulli.bernoulli_add_indicator_eq_sub
-- Module: Mathlib.NumberTheory.Bernoulli
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))
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
⊢ ¬p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den

Tactic:
rw [hT]
-- Module: Mathlib.NumberTheory.Bernoulli
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))
⊢ pIntegral p (↑T : ℚ)

Tactic:
have hT_int : pIntegral p T := Int.padicValuation_le_one p T
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ)
⊢ 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)
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ)
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))
⊢ ¬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:
Rat.padicValuation_le_one_iff.mp ((Rat.padicValuation p).map_sub_le hT_int hR)

Premises used: Valuation.map_sub_le, Iff.mp, Rat.padicValuation, Rat.padicValuation_le_one_iff
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ)
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))
⊢ ¬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:
exact Rat.padicValuation_le_one_iff.mp ((Rat.padicValuation p).map_sub_le hT_int hR)

Premises used: Valuation.map_sub_le, Iff.mp, Rat.padicValuation, Rat.padicValuation_le_one_iff
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
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
⊢ ¬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)

Premises used: _private.0.Bernoulli.bernoulli_add_indicator_eq_sub
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
rw :
  ¬p ∣
      (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
          ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den
⊢ ¬p ∣ (bernoulli (2 * k) + ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den

Tactic:
rw [sum_one_div_prime_eq_indicator_div_add (p := p) hk, ← add_assoc]

Premises used: add_assoc, _private.0.Bernoulli.sum_one_div_prime_eq_indicator_div_add
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ (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
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hcop_ind : (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ)).den.Coprime p
⊢ (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))
-- Module: Mathlib.NumberTheory.Bernoulli
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.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
-- Module: Mathlib.NumberTheory.Bernoulli
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
hcop :
  p.Coprime
    (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
        ∑ i ∈ vonStaudtPrimes k with i ≠ p, HDiv.hDiv (α := ℚ) 1 (↑i : ℚ)).den
⊢ ¬p ∣
      (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
          ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den

Tactic:
(Nat.Prime.coprime_iff_not_dvd Fact.out).1 hcop

Premises used: Iff.mp, Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.NumberTheory.Bernoulli
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
hcop :
  p.Coprime
    (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
        ∑ i ∈ vonStaudtPrimes k with i ≠ p, HDiv.hDiv (α := ℚ) 1 (↑i : ℚ)).den
⊢ ¬p ∣
      (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / (↑p : ℚ) +
          ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den

Tactic:
exact (Nat.Prime.coprime_iff_not_dvd Fact.out).1 hcop

Premises used: Iff.mp, Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ))
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 : ℚ))
⊢ 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

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ (↑1 : ℚ) =
    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:
decide +kernel
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ 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:
exact ⟨1, by decide +kernel⟩
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ)

Tactic:
⟨_, Rat.coe_int_num_of_den_eq_one ?_⟩

Premises used: Rat.coe_int_num_of_den_eq_one, Exists.intro
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k : ℕ
hk : k > 0
inr :
  (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)).den = 1
⊢ ∃ (y : ℤ),
    (↑y : ℚ) =
      bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)

Tactic:
refine ⟨_, Rat.coe_int_num_of_den_eq_one ?_⟩
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k : ℕ
hk : k > 0
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
⊢ (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, HDiv.hDiv (α := ℚ) 1 (↑p : ℚ)).den = 1

Tactic:
by_contra h
-- Module: Mathlib.NumberTheory.Bernoulli
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
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
⊢ False

Tactic:
obtain ⟨p, hp, hdvd⟩ := ne_one_iff_exists_prime_dvd.mp h

Premises used: Nat.ne_one_iff_exists_prime_dvd, Iff.mp
-- Module: Mathlib.NumberTheory.Bernoulli
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
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:
(let : Fact p.Prime := ⟨hp⟩; not_dvd_den_vonStaudt_sum hk) hdvd

Premises used: Fact.mk, _private.0.Bernoulli.not_dvd_den_vonStaudt_sum
-- Module: Mathlib.NumberTheory.Bernoulli
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
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:
exact (let : Fact p.Prime := ⟨hp⟩; not_dvd_den_vonStaudt_sum hk) hdvd

Premises used: Fact.mk, _private.0.Bernoulli.not_dvd_den_vonStaudt_sum
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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)) : ℚ)))
⊢ bernoulli n = ∑ i ∈ range (n + 1), (monomial i : (a : ℚ) → ℚ[X]) (_root_.bernoulli (n - i) * (↑(n.choose i) : ℚ))

Tactic:
rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]

Premises used: Polynomial.bernoulli, Finset.sum_range_reflect, Nat.add_succ_sub_one, add_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
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])
⊢ 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:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
hx : x ∈ range (n + 1)
⊢ x ≤ n

Tactic:
rw [mem_range_succ_iff] at hx

Premises used: Finset.mem_range_succ_iff
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n x : ℕ
hx : x ≤ n
rw :
  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 x) : ℚ)) : ℚ[X])
rw₁ rw₂ :
  Eq (α := ℚ[X]) ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
    ((monomial (n - x) : (a : ℚ) → ℚ[X]) (_root_.bernoulli x * (↑(n.choose x) : ℚ)) : ℚ[X])
⊢ 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:
rw [choose_symm hx, tsub_tsub_cancel_of_le hx]

Premises used: Nat.choose_symm, tsub_tsub_cancel_of_le
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
simp :
  (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    if i ≤ n then _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ) else 0
⊢ (bernoulli n).coeff i = if i ≤ n then _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ) else 0

Tactic:
simp only [bernoulli, finsetSum_coeff, coeff_monomial]

Premises used: Polynomial.bernoulli, Polynomial.finsetSum_coeff, Polynomial.coeff_monomial
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
pos :
  ∀ (h : i ≤ n),
    (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
      _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ)
neg :
  ∀ (h : ¬i ≤ n), Eq (α := ℚ) (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) 0
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    if i ≤ n then _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : i ≤ n
⊢ n - i ∈ range (n + 1)

Tactic:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : i ≤ n
h₁ : ∀ x ∈ range (n + 1), n - x = i ↔ n - i = x
h₂ : n.choose i = n.choose (n - i)
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) =
    _root_.bernoulli (n - i) * (↑(n.choose i) : ℚ)

Tactic:
convert! sum_ite_eq_of_mem (range (n + 1)) (n - i) _ (by grind) using 3

Premises used: HSub.hSub, Finset.sum_ite_eq_of_mem, Finset.range, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : i ≤ n
x : ℕ
h_1 : x ∈ range (n + 1)
⊢ n - x = i ↔ n - i = x

Tactic:
grind [choose_symm]

Premises used: Nat.choose_symm
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : i ≤ n
⊢ n.choose i = n.choose (n - i)

Tactic:
grind [choose_symm]

Premises used: Nat.choose_symm
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : ¬i ≤ n
⊢ ∀ x ∈ range (n + 1), (if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n i : ℕ
h : ¬i ≤ n
⊢ Eq (α := ℚ) (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * (↑(n.choose x) : ℚ) else 0) 0

Tactic:
exact Finset.sum_eq_zero <| by grind

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
⊢ bernoulli 0 = 1

Tactic:
simp [bernoulli]

Premises used: Polynomial.bernoulli
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
⊢ bernoulli 1 = HSub.hSub (α := ℚ[X]) X ((C : (a : ℚ) → ℚ[X]) 2⁻¹)

Tactic:
simp [bernoulli, ← smul_X_eq_monomial, sum_range_succ, ← C_1, -map_one, neg_div, sub_eq_add_neg]

Premises used: Polynomial.C_1, neg_div, Polynomial.bernoulli, sub_eq_add_neg, map_one, Polynomial.smul_X_eq_monomial, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
rw : (bernoulli n).coeff 0 = _root_.bernoulli n
rw₁ : (if 0 ≤ n then _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) else 0) = _root_.bernoulli n
rw₂ : _root_.bernoulli (n - 0) * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
rw₃ : _root_.bernoulli n * (↑(n.choose 0) : ℚ) = _root_.bernoulli n
rw₄ : _root_.bernoulli n * (↑1 : ℚ) = _root_.bernoulli n
rw₅ : _root_.bernoulli n * 1 = _root_.bernoulli n
rw₆ rw₇ : _root_.bernoulli n = _root_.bernoulli n
⊢ eval 0 (bernoulli n) = _root_.bernoulli n

Tactic:
rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
    Nat.choose_zero_right, Nat.cast_one, mul_one]

Premises used: Nat.zero_le, Polynomial.coeff_zero_eq_eval_zero, if_pos, Nat.sub_zero, mul_one, Polynomial.coeff_bernoulli, Nat.cast_one, Nat.choose_zero_right
-- Module: Mathlib.NumberTheory.BernoulliPolynomials
Goal:
n : ℕ
simp :
  ∑ i ∈ range (n + 1), eval 1 ((monomial (n - i) : (a : ℚ) → ℚ[X]) (_root_.bernoulli i * (↑(n.choose i) : ℚ))) =
    bernoulli' n
⊢ eval 1 (bernoulli n) = bernoulli' n

Tactic:
simp only [bernoulli, eval_finsetSum]

Premises used: Polynomial.bernoulli, Polynomial.eval_finsetSum