awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        ((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)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ pIntegral p
    ((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))
have hy : LE.le (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
      (vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: apply (Rat.padicValuation p).map_sub_le
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        ((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)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have hx : LE.le (α := WithZero (Multiplicative ℤ))
  ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
      ((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))) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [mul_assoc, mul_div_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    ((Rat.padicValuation p : (a : ℚ) → WithZero (Multiplicative ℤ))
        ((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))) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
have hx : pIntegral p
  ((↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
    (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
Tactic: apply pIntegral_mul ih
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
⊢ (↑((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))
have rw : (↑((2 * k).choose (2 * m)) : ℚ) * (P * (↑p : ℚ)) / (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))
Tactic: rw [hpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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)
⊢ pIntegral p
    ((↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
have 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))
Tactic: have hpow_mul : ((2 * k).choose (2 * m) : ℚ) * (p : ℚ) ^ (2 * k - 2 * m) /
        (2 * k - 2 * m + 1) =
        (p : ℚ) * (((2 * k).choose (2 * m) : ℚ) * P / (2 * k - 2 * m + 1)) := by
      rw [hpow]; ring
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
    ((↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
have hx : pIntegral p
  ((↑p : ℚ) *
    ((↑((2 * k).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1)))
Tactic: rw [H, hpow_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
⊢ 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 ℤ))
have 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 ℤ))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
Tactic: split_ifs
-- 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 : ℚ))
⊢ pIntegral 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)),
  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: refine (Rat.padicValuation p).map_sum_le fun i hi ↦ ?_
-- 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 ∈ 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 ℤ))
have hi₁ : i < 2 * k
Tactic: rw [Finset.mem_range] at hi
Cleared hypotheses: hi
-- 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 < 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 ℤ))
have 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 ℤ))
Tactic: rcases i with _ | _ | i
Cleared hypotheses: i, hi
-- 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 < 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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
Tactic: rcases i with _ | _ | i
Cleared hypotheses: i, hi
-- 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 < 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 ℤ))
⊢ 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 ℤ))
have 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 ℤ))
Tactic: rcases i with _ | _ | i
Cleared hypotheses: i, hi
-- 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 : 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 ℤ))
have 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 ℤ))
Tactic: simp only [bernoulli_zero, one_mul, Nat.choose_zero_right, Nat.cast_one, Nat.sub_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
⊢ 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 ℤ))
have 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 ℤ))
Tactic: rw [zero_add, Nat.choose_one_right, bernoulli_one]