awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ p ^ (m - 1) + 1 ≤ p ^ (m - 1) * p
have nlinarith : p ^ (m - 1) * p < p ^ (m - 1) + 1 →
  HMul.hMul (α := ℤ) 2 (-1) + 2 * HSub.hSub (α := ℤ) 2 (↑p : ℤ) +
          2 * (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) * (↑p : ℤ) + 1 - (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) + 1)) +
        (0 - HSub.hSub (α := ℤ) 0 (↑p : ℤ) * (1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1))) +
      (0 - HSub.hSub (α := ℤ) 2 (↑p : ℤ) * (1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1))) =
    0
Tactic: nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
nlinarith :
  p ^ (m - 1) * p < p ^ (m - 1) + 1 →
    HMul.hMul (α := ℤ) 2 (-1) + 2 * HSub.hSub (α := ℤ) 2 (↑p : ℤ) +
            2 * (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) * (↑p : ℤ) + 1 - (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) + 1)) +
          (0 - HSub.hSub (α := ℤ) 0 (↑p : ℤ) * (1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1))) +
        (0 - HSub.hSub (α := ℤ) 2 (↑p : ℤ) * (1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1))) =
      0
⊢ p ^ (m - 1) + 1 ≤ p ^ (m - 1) * p
have nlinarith₁ : p ^ (m - 1) * p < p ^ (m - 1) + 1 → GT.gt (α := ℤ) 2 0
Tactic: nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ p ^ (m - 1) * p = p ^ m
have rw : p ^ (m - 1 + 1 - 1) * p = p ^ (m - 1 + 1)
Tactic: rw [show m = m - 1 + 1 by lia]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)
have calc : m + 1 + 1 ≤ p ^ (m - 1) + 1
Tactic: calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
calc : m + 1 + 1 ≤ p ^ (m - 1) + 1
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)
have calc₁ : p ^ (m - 1) + 1 ≤ p ^ (m - 1) * p
Tactic: calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
calc : m + 1 + 1 ≤ p ^ (m - 1) + 1
calc₁ : p ^ (m - 1) + 1 ≤ p ^ (m - 1) * p
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)
have calc₂ : p ^ (m - 1) * p = p ^ m
Tactic: calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hn : n ≥ 2
hne' : ¬(p = 2 ∧ n = 2)
⊢ n + 1 ≤ p ^ (n - 1)
have neg : ∀ (hne' : ¬(p = 2 ∧ Eq (α := ℕ) 2 2)), HAdd.hAdd (α := ℕ) 2 1 ≤ p ^ HSub.hSub (α := ℕ) 2 1
Tactic: induction hn with
    | refl => norm_num at hne' ⊢; lia
    | @step m hm IH =>
      by_cases hm2 : p = 2 ∧ m = 2
      · obtain ⟨rfl, rfl⟩ := hm2; norm_num
      · calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..
Cleared hypotheses: hn, hne'
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n : ℕ
hn : n ≥ 2
hne' : ¬(p = 2 ∧ n = 2)
neg : ∀ (hne' : ¬(p = 2 ∧ Eq (α := ℕ) 2 2)), HAdd.hAdd (α := ℕ) 2 1 ≤ p ^ HSub.hSub (α := ℕ) 2 1
⊢ n + 1 ≤ p ^ (n - 1)
have neg₁ : ∀ {m : ℕ} (hm : Nat.le 2 m) (IH : ∀ (hne' : ¬(p = 2 ∧ m = 2)), m + 1 ≤ p ^ (m - 1)) (hne' : ¬(p = 2 ∧ m.succ = 2)),
  m.succ + 1 ≤ p ^ (m.succ - 1)
Tactic: induction hn with
    | refl => norm_num at hne' ⊢; lia
    | @step m hm IH =>
      by_cases hm2 : p = 2 ∧ m = 2
      · obtain ⟨rfl, rfl⟩ := hm2; norm_num
      · calc m + 1 + 1 ≤ p ^ (m - 1) + 1 := by linarith [IH hm2]
          _ ≤ p ^ (m - 1) * p := by nlinarith [Nat.one_le_pow (m - 1) p (by lia)]
          _ = p ^ m := by rw [show m = m - 1 + 1 by lia]; exact pow_succ ..
Cleared hypotheses: hn, hne'
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1 ≠ 0
have norm_cast : ¬False
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 ≠ 0
have norm_cast : ¬Int.subNatNat (2 * k) (2 * m) + 1 = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ (↑((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)
have rw : (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) * x =
  (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * x
Tactic: rw [div_eq_div_iff (by norm_cast) (by norm_cast; lia), mul_right_comm _ x, mul_right_comm _ x]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) * x =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1) * x
have refine : (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) =
  (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
Tactic: refine congrArg (· * x) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 = (↑(2 * k + 1 - 2 * m) : ℚ)
have norm_cast : Int.subNatNat (2 * k) (2 * m) + 1 = (↑(2 * k + 1 - 2 * m) : ℤ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ (↑((2 * k + 1).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1) =
    (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
have rw : HMul.hMul (α := ℚ) (↑((2 * k + 1).choose (2 * m)) : ℚ) (↑(2 * k + 1 - 2 * m) : ℚ) =
  (↑((2 * k).choose (2 * m)) : ℚ) * (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1)
Tactic: rw [show (2 * (k : ℚ) - 2 * (m : ℚ) + 1) = (↑(2 * k + 1 - 2 * m) : ℚ) by norm_cast; lia]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k m p : ℕ
hm_lt : m < k
inst : Fact (Nat.Prime p)
hd : 2 * k - 2 * m ≥ 2
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
have set : let d := 2 * k - 2 * m;
∀ (hd : d ≥ 2) (hd_def : d = 2 * k - 2 * m),
  pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
Tactic: set d := 2 * k - 2 * m with hd_def
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
have hd_plus_one_ne_zero : d + 1 ≠ 0
Tactic: have ⟨hd_plus_one_ne_zero, h_exp, hkm⟩ :
      d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
have h_exp : 2 * k - 2 * m - 1 = d - 1
Tactic: have ⟨hd_plus_one_ne_zero, h_exp, hkm⟩ :
      d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
have hkm : 2 * m ≤ 2 * k
Tactic: have ⟨hd_plus_one_ne_zero, h_exp, hkm⟩ :
      d + 1 ≠ 0 ∧ 2 * k - 2 * m - 1 = d - 1 ∧ 2 * m ≤ 2 * k := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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 = (↑(2 * k - 2 * m + 1) : ℚ)
have push_cast : HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1 =
  HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1
Tactic: push_cast [Nat.cast_sub hkm]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ pIntegral p
    ((↑((2 * k).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
have h_denom_rat : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) - HMul.hMul (α := ℚ) 2 (↑m : ℚ) + 1))
have rw : pIntegral p ((↑((2 * k).choose (2 * m)) : ℚ) * (HPow.hPow (α := ℚ) (↑p : ℚ) (d - 1) / (↑(d + 1) : ℚ)))
Tactic: rw [h_exp, h_denom_rat, mul_div_assoc]
-- 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 : ℚ))
⊢ pIntegral p
    (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
have hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: have hp_ne : (p : ℚ) ≠ 0 := mod_cast (Nat.Prime.ne_zero Fact.out)
-- 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 (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
have rw : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1 + 1) = P * (↑p : ℚ)
Tactic: rw [show 2 * k - 2 * m = (2 * k - 2 * m - 1) + 1 by lia, pow_succ]
-- 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)
rw : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1 + 1) = P * (↑p : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) = P * (↑p : ℚ)
have rw₁ : HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m - 1) * (↑p : ℚ) = P * (↑p : ℚ)
Tactic: rw [show 2 * k - 2 * m = (2 * k - 2 * m - 1) + 1 by lia, pow_succ]
-- 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)
⊢ pIntegral p
    (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
have hpow : 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]
-- 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 : ℚ)
⊢ 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)
have 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)
Tactic: rw [hpow]
-- 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 : ℚ)
⊢ 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)
have 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)
Tactic: field_simp [hp_ne]
-- 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 : ℚ)
⊢ pIntegral p
    (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
have 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)
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
-- 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)
⊢ pIntegral p
    (bernoulli (2 * m) * (↑((2 * k + 1).choose (2 * m)) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) (2 * k - 2 * m) /
      (HMul.hMul (α := ℚ) 2 (↑k : ℚ) + 1))
have 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))
Tactic: rw [hdecomp]
-- 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)
⊢ 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 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))
Tactic: have hcmp := pIntegral_choose_mul_pow_div (p := p) hm_lt (by lia)
-- 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))
⊢ 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 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)
Tactic: have H x := choose_two_mul_succ_mul_div_eq x hm_lt
-- 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)
⊢ 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 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: apply (Rat.padicValuation p).map_sub_le