awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(d + 1) : ℚ)

Tactic:
have h_denom_rat : (2 * (k : ℚ) - 2 * m + 1) = ((d + 1 : ℕ) : ℚ) := by
    simp only [hd_def]; push_cast [Nat.cast_sub hkm]; ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(d + 1) : ℚ)
rw : pIntegral p ((↑((2 * k).choose (2 * m)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) / (↑(d + 1) : ℚ)))
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))

Tactic:
rw [h_exp, h_denom_rat, mul_div_assoc]

Premises used: mul_div_assoc
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(d + 1) : ℚ)
⊢ pIntegral p ((↑((2 * k).choose (2 * m)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) / (↑(d + 1) : ℚ)))

Tactic:
pIntegral_mul (mod_cast Int.padicValuation_le_one p ((2 * k).choose (2 * m)))
    (pIntegral_pow_div hd_plus_one_ne_zero (factorization_succ_le_sub_one hd))

Premises used: Nat.choose, HMul.hMul, cast, _private.0.Bernoulli.pIntegral_pow_div, Nat.cast, _private.0.Bernoulli.pIntegral, _private.0.Bernoulli.factorization_succ_le_sub_one, Eq.refl, OfNat.ofNat, 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)
d : ℕ := 2 * k - 2 * m
hd : d ≥ 2
hd_def : d = 2 * k - 2 * m
hd_plus_one_ne_zero : d + 1 ≠ 0
h_exp : 2 * k - 2 * m - 1 = d - 1
hkm : 2 * m ≤ 2 * k
h_denom_rat : HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(d + 1) : ℚ)
⊢ pIntegral p ((↑((2 * k).choose (2 * m)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) / (↑(d + 1) : ℚ)))

Tactic:
exact pIntegral_mul (mod_cast Int.padicValuation_le_one p ((2 * k).choose (2 * m)))
    (pIntegral_pow_div hd_plus_one_ne_zero (factorization_succ_le_sub_one hd))

Premises used: _private.0.Bernoulli.pIntegral_pow_div, _private.0.Bernoulli.factorization_succ_le_sub_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 : ℚ))
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Nat.Prime.ne_zero Fact.out)
-- 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)
⊢ 2 * k - 2 * m = 2 * k - 2 * m - 1 + 1

Tactic:
lia
-- 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)
rw : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1 + 1) = P * (↑p : ℚ)
rw₁ rw₂ : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) * (↑p : ℚ) = P * (↑p : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)

Tactic:
rw [show 2 * k - 2 * m = (2 * k - 2 * m - 1) + 1 by lia, pow_succ]

Premises used: pow_succ
-- 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 (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)

Tactic:
have hpow : (p : ℚ) ^ (2 * k - 2 * m) = P * p := by
    rw [show 2 * k - 2 * m = (2 * k - 2 * m - 1) + 1 by lia, pow_succ]
-- 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 : ℚ)
rw :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * (P * (↑p : ℚ)) / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          (P * (↑p : ℚ)) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
⊢ 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)

Tactic:
rw [hpow]
-- 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 : ℚ)
field_simp :
  bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P * (↑p : ℚ) =
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * P *
      (bernoulli (2 * m) * (↑p : ℚ) + vonStaudtIndicator (2 * m) p - vonStaudtIndicator (2 * m) p)
⊢ bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * (P * (↑p : ℚ)) / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / (↑p : ℚ)) * (↑((2 * k + 1).choose (2 * m)) : ℚ) *
          (P * (↑p : ℚ)) /
        (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) -
      vonStaudtIndicator (2 * m) p * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P / (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)

Tactic:
field_simp [hp_ne]
-- 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 : ℚ)
⊢ bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * P * (↑p : ℚ) =
    (↑((2 * k + 1).choose (2 * m)) : ℚ) * P *
      (bernoulli (2 * m) * (↑p : ℚ) + vonStaudtIndicator (2 * m) p - vonStaudtIndicator (2 * m) p)

Tactic:
ring
-- 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 : ℚ)
⊢ 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)

Tactic:
have hdecomp : bernoulli (2 * m) * ((2 * k + 1).choose (2 * m)) *
      (p : ℚ) ^ (2 * k - 2 * m) / (2 * k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / p) *
      ((2 * k + 1).choose (2 * m)) * (p : ℚ) ^ (2 * k - 2 * m) / (2 * k + 1) -
    vonStaudtIndicator (2 * m) p * ((2 * k + 1).choose (2 * m)) *
      P / (2 * k + 1) := by rw [hpow]; field_simp [hp_ne]; ring
-- 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)
rw :
  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))
⊢ pIntegral p
    (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))

Tactic:
rw [hdecomp]
-- 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)
⊢ 2 * k - 2 * m ≥ 2

Tactic:
lia
-- 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)
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))

Tactic:
have hcmp := pIntegral_choose_mul_pow_div (p := p) hm_lt (by lia)
-- 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))
⊢ ∀ (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)

Tactic:
have H x := choose_two_mul_succ_mul_div_eq x hm_lt
-- 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)
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 ℤ))
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 ℤ))
⊢ 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))

Tactic:
apply (Rat.padicValuation p).map_sub_le

Premises used: Valuation.map_sub_le, Rat.padicValuation
-- 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)
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 ℤ))
⊢ 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]

Premises used: mul_assoc, mul_div_assoc
-- 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)
hx :
  pIntegral p
    ((↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 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 ℤ))

Tactic:
apply pIntegral_mul ih

Premises used: _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)
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))
⊢ (↑((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:
rw [hpow]
-- 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)
⊢ (↑((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:
ring
-- 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)
⊢ (↑((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