awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
P : ℚ := HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1)
hpow : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
hdecomp :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
hcmp :
  pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
H :
  ∀ (x : ℚ),
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
      (↑((2 * k).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)
hpow_mul :
  (↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) =
    (↑p : ℚ) *
      ((↑((2 * k).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
hx :
  pIntegral p
    ((↑p : ℚ) *
      ((↑((2 * k).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)))
⊢ pIntegral p
    ((↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))

Tactic:
rw [H, hpow_mul]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
P : ℚ := HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1)
hpow : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
hdecomp :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
hcmp :
  pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
H :
  ∀ (x : ℚ),
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
      (↑((2 * k).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)
hpow_mul :
  (↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) =
    (↑p : ℚ) *
      ((↑((2 * k).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
⊢ pIntegral p
    ((↑p : ℚ) *
      ((↑((2 * k).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)))

Tactic:
pIntegral_mul (Int.padicValuation_le_one p p) hcmp

Premises used: Nat.cast, Int.padicValuation_le_one, _private.0.Bernoulli.pIntegral_mul
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
P : ℚ := HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1)
hpow : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
hdecomp :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
hcmp :
  pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
H :
  ∀ (x : ℚ),
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
      (↑((2 * k).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)
hpow_mul :
  (↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) =
    (↑p : ℚ) *
      ((↑((2 * k).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
⊢ pIntegral p
    ((↑p : ℚ) *
      ((↑((2 * k).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)))

Tactic:
exact pIntegral_mul (Int.padicValuation_le_one p p) hcmp

Premises used: Nat.cast, Int.padicValuation_le_one, _private.0.Bernoulli.pIntegral_mul
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
P : ℚ := HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1)
hpow : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
hdecomp :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
hcmp :
  pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
H :
  ∀ (x : ℚ),
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
      (↑((2 * k).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)
pos :
  p - 1 ∣ 2 * m →
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
          (HMul.hMul (α := ℚ) 1 (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
neg :
  ¬p - 1 ∣ 2 * m →
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
          (HMul.hMul (α := ℚ) 0 (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (HMul.hMul (α := ℚ) (if p - 1 ∣ 2 * m then 1 else 0) (↑((2 * k + 1).choose (2 * m)) : ℚ) * P /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
P : ℚ := HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1)
hpow : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
hdecomp :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
hcmp :
  pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
H :
  ∀ (x : ℚ),
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
      (↑((2 * k).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)
h : p - 1 ∣ 2 * m
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (HMul.hMul (α := ℚ) 1 (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
grind
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ))
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
P : ℚ := HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1)
hpow : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
hdecomp :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
hcmp :
  pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
H :
  ∀ (x : ℚ),
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
      (↑((2 * k).choose (2 * m)) : ℚ) * x / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)
h : ¬p - 1 ∣ 2 * m
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (HMul.hMul (α := ℚ) 0 (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp
-- 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 : ℚ))
⊢ 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:
(Rat.padicValuation p).map_sum_le fun i hi ↦ ?_

Premises used: Rat.padicValuation, Valuation.map_sum_le
-- 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 : ℚ))
refine :
  ∀ (i : ℕ) (hi : i ∈ range (2 * k)),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
          (bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
⊢ 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:
refine (Rat.padicValuation p).map_sum_le fun i hi ↦ ?_

Premises used: Rat.padicValuation, Valuation.map_sum_le
-- 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 ∈ range (2 * k)
⊢ i < 2 * k

Tactic:
rw [Finset.mem_range] at hi

Premises used: Finset.mem_range
-- 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 < 2 * k
zero :
  ∀ (hi : 0 < 2 * k),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
          (bernoulli 0 * (↑((2 * k + 1).choose 0) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 0) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
succ :
  ∀ (hi : HAdd.hAdd (α := ℕ) 0 1 < 2 * k),
    LE.le (α := WithZero (Multiplicative ℤ))
      ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
          (bernoulli (HAdd.hAdd (α := ℕ) 0 1) * (↑((2 * k + 1).choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) *
              HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - HAdd.hAdd (α := ℕ) 0 1) /
            (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
succ₁ :
  ∀ (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 ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli i * (↑((2 * k + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - i) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rcases i with _ | _ | i
-- 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 : 0 < 2 * k
zero :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k) / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli 0 * (↑((2 * k + 1).choose 0) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 0) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
simp only [bernoulli_zero, one_mul, Nat.choose_zero_right, Nat.cast_one, Nat.sub_zero]

Premises used: bernoulli_zero, Nat.sub_zero, Nat.cast_one, Nat.choose_zero_right, one_mul
-- 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 : 0 < 2 * k
⊢ 2 * k + 1 ≠ 0

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 : ℚ))
hi : 0 < 2 * k
⊢ 2 * k ≥ 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 : ℚ))
hi : 0 < 2 * k
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k) / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
exact_mod_cast pIntegral_pow_div (by lia)
      (factorization_succ_le_sub_one (by lia) |>.trans tsub_le_self)

Premises used: _private.0.Bernoulli.pIntegral_pow_div, tsub_le_self, _private.0.Bernoulli.factorization_succ_le_sub_one, LE.le.trans
-- 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
succ :
  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 ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        (bernoulli (HAdd.hAdd (α := ℕ) 0 1) * (↑((2 * k + 1).choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) *
            HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - HAdd.hAdd (α := ℕ) 0 1) /
          (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [zero_add, Nat.choose_one_right, bernoulli_one]

Premises used: zero_add, Nat.choose_one_right, bernoulli_one
-- 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
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 ℤ))
⊢ 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 ℤ))

Tactic:
push_cast
-- 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
succ :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ 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:
field_simp
-- 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
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 ℤ))
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 ℤ))
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ))
⊢ 2 * k - 1 = 2 * k - 2 + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ))
succ :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation 2 : (a : ℚ) → WithZero (Multiplicative ℤ)) (-HPow.hPow (α := ℚ) 2 (2 * k - 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation 2 : (a : ℚ) → WithZero (Multiplicative ℤ)) (-(HPow.hPow (α := ℚ) 2 (2 * k - 1) / 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]

Premises used: pow_succ, mul_div_cancel_right₀, two_ne_zero
-- Module: Mathlib.NumberTheory.Bernoulli
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 - 2)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
exact_mod_cast Int.padicValuation_le_one ..

Premises used: Int.padicValuation_le_one
-- 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
succ :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (HPow.hPow (α := ℚ) (↑p : ℚ) (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 ℤ))

Tactic:
rw [Valuation.map_neg]

Premises used: Valuation.map_neg
-- 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
⊢ 0 ≤ 2 * k - 1

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 : ℚ))
hi : HAdd.hAdd (α := ℕ) 0 1 < 2 * k
hp2 : p ≠ 2
succ : 2 < p
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ)) (HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 1) / 2) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
refine pIntegral_pow_div two_ne_zero <|
         (factorization_eq_zero_of_lt ?_).trans_le (by lia)

Premises used: _private.0.Bernoulli.pIntegral_pow_div, Eq.trans_le, two_ne_zero, Nat.factorization_eq_zero_of_lt
-- 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:
(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, Nat.lt, Fact.out