awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n p : ℕ
zero :
  Eq (α := ℚ) (∑ k ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (β := ℕ) (↑k : ℚ) 0)
    (∑ i ∈ range (HAdd.hAdd (α := ℕ) 0 1),
      bernoulli' i * (↑((HAdd.hAdd (α := ℕ) 0 1).choose i) : ℚ) *
          HPow.hPow (α := ℚ) (↑n : ℚ) (HAdd.hAdd (α := ℕ) 0 1 - i) /
        (↑(succ 0) : ℚ))
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑k : ℚ) p)
    (∑ i ∈ range (p + 1),
      bernoulli' i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑p.succ : ℚ))
have succ : ∀ (p : ℕ),
  Eq (α := ℚ) (∑ k ∈ Ico 1 (n + 1), HPow.hPow (α := ℚ) (↑k : ℚ) (p + 1))
    (∑ i ∈ range (p + 1 + 1),
      bernoulli' i * (↑((p + 1 + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 + 1 - i) / (↑(p + 1).succ : ℚ))
Tactic: cases p with | zero => simp | succ p =>
  let f i := bernoulli i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
  let f' i := bernoulli' i * p.succ.succ.choose i * (n : ℚ) ^ (p.succ.succ - i) / p.succ.succ
  suffices (∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ) = ∑ i ∈ range p.succ.succ, f' i by convert!
    this
  -- prove some algebraic facts that will make things easier for us later on
  have hle := Nat.le_add_left 1 n
  have hne : (p + 1 + 1 : ℚ) ≠ 0 := by norm_cast
  have h1 : ∀ r : ℚ, r * (p + 1 + 1) * (n : ℚ) ^ p.succ / (p + 1 + 1 : ℚ) = r * (n : ℚ) ^ p.succ :=
      fun r => by rw [mul_div_right_comm, mul_div_cancel_right₀ _ hne]
  have h2 : f 1 + (n : ℚ) ^ p.succ = 1 / 2 * (n : ℚ) ^ p.succ := by
    simp_rw [f, bernoulli_one, choose_one_right, succ_sub_succ_eq_sub, cast_succ, tsub_zero, h1]
    ring
  have :
    (∑ i ∈ range p, bernoulli (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2)) =
      ∑ i ∈ range p, bernoulli' (i + 2) * (p + 2).choose (i + 2) * (n : ℚ) ^ (p - i) / ↑(p + 2) :=
    sum_congr rfl fun i _ => by rw [bernoulli_eq_bernoulli'_of_ne_one (succ_succ_ne_one i)]
  calc
    (-- replace sum over `Ico` with sum over `range` and simplify
        ∑ k ∈ Ico 1 n.succ, (k : ℚ) ^ p.succ)
    _ = ∑ k ∈ range n.succ, (k : ℚ) ^ p.succ := by simp [sum_Ico_eq_sub _ hle]
    -- extract the last term of the sum
    _ = (∑ k ∈ range n, (k : ℚ) ^ p.succ) + (n : ℚ) ^ p.succ := by rw [sum_range_succ]
    -- apply the key lemma, `sum_range_pow`
    _ = (∑ i ∈ range p.succ.succ, f i) + (n : ℚ) ^ p.succ := by simp [f, sum_range_pow]
    -- extract the first two terms of the sum
    _ = (∑ i ∈ range p, f i.succ.succ) + f 1 + f 0 + (n : ℚ) ^ p.succ := by
      simp_rw [sum_range_succ']
    _ = (∑ i ∈ range p, f i.succ.succ) + (f 1 + (n : ℚ) ^ p.succ) + f 0 := by ring
    _ = (∑ i ∈ range p, f i.succ.succ) + 1 / 2 * (n : ℚ) ^ p.succ + f 0 := by rw [h2]
    -- convert from `bernoulli` to `bernoulli'`
    _ = (∑ i ∈ range p, f' i.succ.succ) + f' 1 + f' 0 := by
      simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]
    -- rejoin the first two terms of the sum
    _ = ∑ i ∈ range p.succ.succ, f' i := by simp_rw [sum_range_succ']
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p l : ℕ
inst : Fact (Nat.Prime p)
⊢ HAdd.hAdd (α := ZMod p) (∑ v ∈ Ico 1 p, HPow.hPow (α := ZMod p) (↑v : ZMod p) l) (if p - 1 ∣ l then 1 else 0) = 0
have hbij : Eq (α := ZMod p) (∑ v ∈ Ico 1 p, HPow.hPow (α := ZMod p) (↑v : ZMod p) l) (∑ u : (ZMod p)ˣ, (↑u : ZMod p) ^ l)
Tactic: have hbij : (∑ v ∈ Ico 1 p, (v : ZMod p) ^ l) = ∑ u : (ZMod p)ˣ, (u : ZMod p) ^ l :=
    Finset.sum_bij'
      (fun v hv ↦ Units.mk0 (v : ZMod p) (mt (ZMod.natCast_eq_zero_iff v p).mp (by
        grind [not_dvd_of_pos_of_lt])))
      (fun u _ ↦ (u : ZMod p).val)
      (fun _ _ ↦ Finset.mem_univ _)
      (fun u _ ↦ by grind [u.ne_zero, ZMod.val_ne_zero, ZMod.val_lt])
      (fun v hv ↦ by simp [ZMod.val_cast_of_lt (Finset.mem_Ico.mp hv).2])
      (fun u _ ↦ Units.ext (ZMod.natCast_zmod_val _))
      (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p l : ℕ
inst : Fact (Nat.Prime p)
hbij : Eq (α := ZMod p) (∑ v ∈ Ico 1 p, HPow.hPow (α := ZMod p) (↑v : ZMod p) l) (∑ u : (ZMod p)ˣ, (↑u : ZMod p) ^ l)
⊢ HAdd.hAdd (α := ZMod p) (∑ v ∈ Ico 1 p, HPow.hPow (α := ZMod p) (↑v : ZMod p) l) (if p - 1 ∣ l then 1 else 0) = 0
have rw : HAdd.hAdd (α := ZMod p) (if p - 1 ∣ l then -1 else 0) (if p - 1 ∣ l then 1 else 0) = 0
Tactic: rw [hbij, FiniteField.sum_pow_units, ZMod.card]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
⊢ Coprime (∏ q ∈ vonStaudtPrimes k with q ≠ p, (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den) p
have refine : ∀ (q : ℕ) (hq : q ∈ {q ∈ vonStaudtPrimes k | q ≠ p}), (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
Tactic: refine Nat.Coprime.prod_left fun q hq ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hq : q ∈ {q ∈ vonStaudtPrimes k | q ≠ p}
⊢ (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
have hq₁ : (q < 2 * k + 2 ∧ Nat.Prime q ∧ q - 1 ∣ 2 * k) ∧ q ≠ p
Tactic: simp only [Finset.mem_filter, Finset.mem_range] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hq : (q < 2 * k + 2 ∧ Nat.Prime q ∧ q - 1 ∣ 2 * k) ∧ q ≠ p
⊢ (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
have hne : q ≠ p
Tactic: obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hq : (q < 2 * k + 2 ∧ Nat.Prime q ∧ q - 1 ∣ 2 * k) ∧ q ≠ p
hne : q ≠ p
⊢ (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
have left : q < 2 * k + 2
Tactic: obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hq : (q < 2 * k + 2 ∧ Nat.Prime q ∧ q - 1 ∣ 2 * k) ∧ q ≠ p
hne : q ≠ p
left : q < 2 * k + 2
⊢ (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
have hq_prime : Nat.Prime q
Tactic: obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hq : (q < 2 * k + 2 ∧ Nat.Prime q ∧ q - 1 ∣ 2 * k) ∧ q ≠ p
hne : q ≠ p
left : q < 2 * k + 2
hq_prime : Nat.Prime q
⊢ (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
have right : q - 1 ∣ 2 * k
Tactic: obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hne : q ≠ p
left : q < 2 * k + 2
hq_prime : Nat.Prime q
right : q - 1 ∣ 2 * k
⊢ (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
have rw : q.Coprime p
Tactic: rw [show ((1 : ℚ) / q).den = q by simp [hq_prime.ne_zero]]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ vonStaudtPrimes k with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
have rw : ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
  vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
Tactic: rw [Finset.sum_congr (Finset.filter_ne' (vonStaudtPrimes k) p) fun _ _ ↦ rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
⊢ ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
have pos : ∀ (hdvd : p - 1 ∣ 2 * k),
  ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
Tactic: by_cases hdvd : (p - 1) ∣ 2 * k
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
pos :
  ∀ (hdvd : p - 1 ∣ 2 * k),
    ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
      vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
⊢ ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
have neg : ∀ (hdvd : ¬p - 1 ∣ 2 * k),
  ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
Tactic: by_cases hdvd : (p - 1) ∣ 2 * k
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ p < 2 * k + 2
have this : p - 1 ≤ 2 * k
Tactic: have := Nat.le_of_dvd (by lia) hdvd
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
have hp_mem : p ∈ vonStaudtPrimes k
Tactic: have hp_mem : p ∈ vonStaudtPrimes k := Finset.mem_filter.mpr
      ⟨Finset.mem_range.mpr (by have := Nat.le_of_dvd (by lia) hdvd; lia), Fact.out, hdvd⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
hp_mem : p ∈ vonStaudtPrimes k
⊢ ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
have pos : HDiv.hDiv (α := ℚ) 1 (↑p : ℚ) + ∑ x ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑x : ℚ) =
  vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
Tactic: rw [← Finset.add_sum_erase _ _ hp_mem]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : ¬p - 1 ∣ 2 * k
⊢ ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
have neg : ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
  vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)
Tactic: rw [Finset.erase_eq_of_notMem fun h ↦ hdvd (Finset.mem_filter.mp h).2.2]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))
have hM'_cop : M'.Coprime p
Tactic: have hM'_cop : M'.Coprime p := (Nat.coprime_ordCompl Fact.out hM).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))
have hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
Tactic: have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.Prime.ne_zero Fact.out)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))
have hdecomp : p ^ e * M' = M
Tactic: have hdecomp : p ^ e * M' = M := Nat.ordProj_mul_ordCompl_eq_self M p
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
⊢ (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
have rw : (↑(p ^ e * M') : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
Tactic: rw [← hdecomp]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))
have hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
Tactic: have hM_eq : (M : ℚ) = ↑(p ^ e) * ↑M' := by rw [← hdecomp]; simp
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
have rw : HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e / (↑M' : ℚ) =
  HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
Tactic: rw [hM_eq, Nat.cast_pow, div_mul_eq_div_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e / (↑M' : ℚ) =
    HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
have e_a : HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e)
have e_a : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) * HPow.hPow (α := ℚ) (↑p : ℚ) e
Tactic: rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
e_a : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) * HPow.hPow (α := ℚ) (↑p : ℚ) e
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e)
have e_a₁ : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e + e)
Tactic: rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
e_a : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) * HPow.hPow (α := ℚ) (↑p : ℚ) e
e_a₁ : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e + e)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) N / HPow.hPow (α := ℚ) (↑p : ℚ) e = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e)
have e_a₂ : HPow.hPow (α := ℚ) (↑p : ℚ) N = HPow.hPow (α := ℚ) (↑p : ℚ) N
Tactic: rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))
have hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
Tactic: have hrw : (p : ℚ) ^ N / M = (p : ℚ) ^ (N - e) / M' := by
    rw [hM_eq, Nat.cast_pow, div_mul_eq_div_div]
    congr 1
    rw [div_eq_iff (pow_ne_zero e hp_ne), ← pow_add, Nat.sub_add_cancel hv]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
⊢ HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
have norm_cast : HDiv.hDiv (α := ℚ) (↑(p ^ (N - e)) : ℚ) (↑M' : ℚ) = (↑(NNRat.divNat (p ^ (N - e)) M') : ℚ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))
have hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
Tactic: have hM'_eq : ((p : ℚ) ^ (N - e) / (M' : ℚ)) = Rat.divInt (p ^ (N - e) : ℤ) (M' : ℤ) := by
    norm_cast
    simp
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
⊢ pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ))
have rw : pIntegral p (HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ))
Tactic: rw [hrw]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : Ne (α := ℚ) (↑p : ℚ) 0
hdecomp : p ^ e * M' = M
hM_eq : (↑M : ℚ) = HMul.hMul (α := ℚ) (↑(p ^ e) : ℚ) (↑M' : ℚ)
hrw : HPow.hPow (α := ℚ) (↑p : ℚ) N / (↑M : ℚ) = HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)
hM'_eq : HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ) = Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)
⊢ (HPow.hPow (α := ℚ) (↑p : ℚ) (N - e) / (↑M' : ℚ)).den ∣ M'
have rw : (Rat.divInt (HPow.hPow (α := ℤ) (↑p : ℤ) (N - e)) (↑M' : ℤ)).den ∣ M'
Tactic: rw [hM'_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
⊢ ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
have pos : ∀ (hcase : p = 2 ∧ d = 2), ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
Tactic: by_cases hcase : p = 2 ∧ d = 2
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
pos : ∀ (hcase : p = 2 ∧ d = 2), ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
⊢ ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
have neg : ∀ (hcase : ¬(p = 2 ∧ d = 2)), ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
Tactic: by_cases hcase : p = 2 ∧ d = 2
-- 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
⊢ ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
have pos : ∀ [Fact (Nat.Prime 2)] (hd : GE.ge (α := ℕ) 2 2),
  ((HAdd.hAdd (α := ℕ) 2 1).factorization : (a : ℕ) → ℕ) 2 ≤ HSub.hSub (α := ℕ) 2 1
Tactic: obtain ⟨rfl, rfl⟩ := hcase
Cleared hypotheses: p, d, inst, hd, hcase
-- 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)
⊢ ((d + 1).factorization : (a : ℕ) → ℕ) p ≤ d - 1
have neg : d + 1 ≤ p ^ (d - 1)
Tactic: apply Nat.factorization_le_of_le_pow
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
p d : ℕ
inst : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
⊢ d + 1 ≤ p ^ (d - 1)
have hp2 : 2 ≤ p
Tactic: have hp2 := (Fact.out : p.Prime).two_le
-- 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
⊢ d + 1 ≤ p ^ (d - 1)
have neg : ∀ n ≥ 2, ¬(p = 2 ∧ n = 2) → n + 1 ≤ p ^ (n - 1)
Tactic: suffices ∀ n : ℕ, n ≥ 2 → ¬(p = 2 ∧ n = 2) → n + 1 ≤ p ^ (n - 1) from this d hd hcase
-- 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 : ℕ
hne' : ¬(p = 2 ∧ Eq (α := ℕ) 2 2)
⊢ HAdd.hAdd (α := ℕ) 2 1 ≤ p ^ HSub.hSub (α := ℕ) 2 1
have neg : ∀ (hne' : ¬p = 2), 3 ≤ p
Tactic: norm_num at hne' ⊢
Cleared hypotheses: 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 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)
have pos : ∀ (hm2 : p = 2 ∧ m = 2), m.succ + 1 ≤ p ^ (m.succ - 1)
Tactic: by_cases hm2 : p = 2 ∧ m = 2
-- 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)
pos : ∀ (hm2 : p = 2 ∧ m = 2), m.succ + 1 ≤ p ^ (m.succ - 1)
⊢ m.succ + 1 ≤ p ^ (m.succ - 1)
have neg : ∀ (hm2 : ¬(p = 2 ∧ m = 2)), m.succ + 1 ≤ p ^ (m.succ - 1)
Tactic: by_cases hm2 : p = 2 ∧ m = 2
-- 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 pos : ∀ [Fact (Nat.Prime 2)] (hcase : ¬(Eq (α := ℕ) 2 2 ∧ d = 2)) (hp2 : LE.le (α := ℕ) 2 2) (hm : Nat.le 2 2)
  (IH :
    ∀ (hne' : ¬(Eq (α := ℕ) 2 2 ∧ Eq (α := ℕ) 2 2)),
      HAdd.hAdd (α := ℕ) 2 1 ≤ HPow.hPow (α := ℕ) 2 (HSub.hSub (α := ℕ) 2 1))
  (hne' : ¬(Eq (α := ℕ) 2 2 ∧ succ 2 = 2)), succ 2 + 1 ≤ HPow.hPow (α := ℕ) 2 (succ 2 - 1)
Tactic: obtain ⟨rfl, rfl⟩ := hm2
Cleared hypotheses: p, inst, hcase, hp2, m, hm, IH, hne', hm2
-- 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 + 1 + 1 ≤ p ^ (m - 1) + 1
have linarith : p ^ (m - 1) + 1 < m + 1 + 1 →
  -1 + (HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1) + 1 + 1 - (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 + 1)) +
      (HAdd.hAdd (α := ℤ) (↑m : ℤ) 1 - HPow.hPow (α := ℤ) (↑p : ℤ) (m - 1)) =
    0
Tactic: linarith [IH hm2]