awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ Eq (α := ℚ) (∑ k ∈ Ico 1 n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)
    (∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ)

Tactic:
simp [sum_Ico_eq_sub _ hle]

Premises used: Finset.sum_Ico_eq_sub
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
rw rw₁ :
  ∑ x ∈ range n, HPow.hPow (α := ℚ) (↑x : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
⊢ ∑ k ∈ range n.succ, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ =
    ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ

Tactic:
rw [sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ ∑ k ∈ range n, HPow.hPow (α := ℚ) (↑k : ℚ) p.succ + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ

Tactic:
simp [f, sum_range_pow]

Premises used: sum_range_pow
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ ∑ i ∈ range p.succ.succ, f i + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ

Tactic:
simp_rw [sum_range_succ']

Premises used: Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ =
    ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0

Tactic:
ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
rw rw₁ :
  ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0 =
    ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0
⊢ ∑ i ∈ range p, f i.succ.succ + (f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ) + f 0 =
    ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0

Tactic:
rw [h2]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ ∑ i ∈ range p, f i.succ.succ + 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ + f 0 =
    ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0

Tactic:
simpa [f, f', h1, fun i => show i + 2 = i + 1 + 1 from rfl]

Premises used: rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
f : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
f' : (i : ℕ) → ℚ :=
  fun (i : ℕ) ↦
    bernoulli' i * (↑(p.succ.succ.choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p.succ.succ - i) / (↑p.succ.succ : ℚ)
hle : 1 ≤ n + 1
hne : HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1 ≠ 0
h1 :
  ∀ (r : ℚ),
    r * (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ / (HAdd.hAdd (α := ℚ) (↑p : ℚ) 1 + 1) =
      r * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
h2 : f 1 + HPow.hPow (α := ℚ) (↑n : ℚ) p.succ = 1 / 2 * HPow.hPow (α := ℚ) (↑n : ℚ) p.succ
this :
  Eq (α := ℚ)
    (∑ i ∈ range p,
      bernoulli (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
    (∑ i ∈ range p,
      bernoulli' (i + 2) * (↑((p + 2).choose (i + 2)) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p - i) / (↑(p + 2) : ℚ))
⊢ ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0 = ∑ i ∈ range p.succ.succ, f' i

Tactic:
simp_rw [sum_range_succ']

Premises used: Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
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) /
        (↑(Nat.succ 0) : ℚ))
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 : ℚ))
⊢ 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 : ℚ))

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']

Premises used: Finset.Ico, Nat.cast, Finset.range, HPow.hPow, Nat.zero, OfNat.ofNat, Nat.succ, Finset.sum
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p l : ℕ
inst : Fact (Nat.Prime p)
v : ℕ
hv : v ∈ Ico 1 p
⊢ ¬p ∣ v

Tactic:
grind [not_dvd_of_pos_of_lt]

Premises used: Nat.not_dvd_of_pos_of_lt
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p l : ℕ
inst : Fact (Nat.Prime p)
u : (ZMod p)ˣ
h : Membership.mem (γ := Finset (ZMod p)ˣ) univ u
⊢ (fun (u : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ u) ↦ (↑u : ZMod p).val) u h ∈ Ico 1 p

Tactic:
grind [u.ne_zero, ZMod.val_ne_zero, ZMod.val_lt]

Premises used: Units.ne_zero, ZMod.val_ne_zero, ZMod.val_lt
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p l : ℕ
inst : Fact (Nat.Prime p)
v : ℕ
hv : v ∈ Ico 1 p
⊢ (fun (u : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ u) ↦ (↑u : ZMod p).val)
      ((fun (v : ℕ) (hv : v ∈ Ico 1 p) ↦ Units.mk0 (↑v : ZMod p) ⋯) v hv) ⋯ =
    v

Tactic:
simp [ZMod.val_cast_of_lt (Finset.mem_Ico.mp hv).2]

Premises used: ZMod.val_cast_of_lt, And.right, Iff.mp, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p l : ℕ
inst : Fact (Nat.Prime p)
⊢ 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)
-- Module: Mathlib.NumberTheory.Bernoulli
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)
rw : HAdd.hAdd (α := ZMod p) (if p - 1 ∣ l then -1 else 0) (if p - 1 ∣ l then 1 else 0) = 0
⊢ 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

Tactic:
rw [hbij, FiniteField.sum_pow_units, ZMod.card]

Premises used: FiniteField.sum_pow_units, ZMod.card
-- Module: Mathlib.NumberTheory.Bernoulli
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) (if p - 1 ∣ l then -1 else 0) (if p - 1 ∣ l then 1 else 0) = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x y : ℚ
hx : pIntegral p x
hy : pIntegral p y
⊢ pIntegral p (x * y)

Tactic:
((Rat.padicValuation p).map_mul x y).trans_le (mul_le_one' hx hy)

Premises used: Eq.trans_le, Valuation.map_mul, Rat.padicValuation, mul_le_one'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
⊢ Coprime (∏ q ∈ vonStaudtPrimes k with q ≠ p, (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den) p

Tactic:
Nat.Coprime.prod_left fun q hq ↦ ?_

Premises used: Nat.Coprime.prod_left
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
refine : ∀ (q : ℕ) (hq : q ∈ {q ∈ vonStaudtPrimes k | q ≠ p}), (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p
⊢ Coprime (∏ q ∈ vonStaudtPrimes k with q ≠ p, (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den) p

Tactic:
refine Nat.Coprime.prod_left fun q hq ↦ ?_

Premises used: Nat.Coprime.prod_left
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hq : q ∈ {q ∈ vonStaudtPrimes k | q ≠ p}
⊢ (q < 2 * k + 2 ∧ Nat.Prime q ∧ q - 1 ∣ 2 * k) ∧ q ≠ p

Tactic:
simp only [Finset.mem_filter, Finset.mem_range] at hq

Premises used: Finset.mem_range, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
inst : Fact (Nat.Prime p)
q : ℕ
hq : (q < 2 * k + 2 ∧ Nat.Prime q ∧ q - 1 ∣ 2 * k) ∧ q ≠ p
⊢ q ≠ p

Tactic:
obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ q < 2 * k + 2

Tactic:
obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ Nat.Prime q

Tactic:
obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ q - 1 ∣ 2 * k

Tactic:
obtain ⟨⟨_, hq_prime, _⟩, hne⟩ := hq
-- Module: Mathlib.NumberTheory.Bernoulli
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 = q

Tactic:
simp [hq_prime.ne_zero]

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.NumberTheory.Bernoulli
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
rw : q.Coprime p
⊢ (HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)).den.Coprime p

Tactic:
rw [show ((1 : ℚ) / q).den = q by simp [hq_prime.ne_zero]]
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ q.Coprime p

Tactic:
(Nat.coprime_primes hq_prime Fact.out).mpr hne

Premises used: Iff.mpr, Fact.out, Nat.coprime_primes
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ q.Coprime p

Tactic:
exact (Nat.coprime_primes hq_prime Fact.out).mpr hne

Premises used: Iff.mpr, Fact.out, Nat.coprime_primes
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
rw :
  ∑ 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 with q ≠ p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)

Tactic:
rw [Finset.sum_congr (Finset.filter_ne' (vonStaudtPrimes k) p) fun _ _ ↦ rfl]

Premises used: _private.0.Bernoulli.vonStaudtPrimes, Finset.filter_ne', Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
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 : ℚ)
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 : ℚ)
⊢ ∑ 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

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ 0 < 2 * k

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ p - 1 ≤ 2 * k

Tactic:
have := Nat.le_of_dvd (by lia) hdvd
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
this : p - 1 ≤ 2 * k
⊢ p < 2 * k + 2

Tactic:
lia
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
⊢ 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⟩
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
hp_mem : p ∈ vonStaudtPrimes k
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 : ℚ)
⊢ ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ (vonStaudtPrimes k).erase p, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)

Tactic:
rw [← Finset.add_sum_erase _ _ hp_mem]

Premises used: Finset.add_sum_erase
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : p - 1 ∣ 2 * k
hp_mem : p ∈ vonStaudtPrimes k
⊢ 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:
simp [vonStaudtIndicator, hdvd]

Premises used: _private.0.Bernoulli.vonStaudtIndicator
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
k p : ℕ
hk : k > 0
inst : Fact (Nat.Prime p)
hdvd : ¬p - 1 ∣ 2 * k
neg :
  ∑ q ∈ vonStaudtPrimes k, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ) =
    vonStaudtIndicator (2 * k) p / (↑p : ℚ) + ∑ q ∈ vonStaudtPrimes k, 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 : ℚ)

Tactic:
rw [Finset.erase_eq_of_notMem fun h ↦ hdvd (Finset.mem_filter.mp h).2.2]

Premises used: Finset.erase_eq_of_notMem
-- Module: Mathlib.NumberTheory.Bernoulli
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, HDiv.hDiv (α := ℚ) 1 (↑q : ℚ)

Tactic:
simp [vonStaudtIndicator, hdvd]

Premises used: _private.0.Bernoulli.vonStaudtIndicator
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
hv : (M.factorization : (a : ℕ) → ℕ) p ≤ N
⊢ let e : ℕ := (M.factorization : (a : ℕ) → ℕ) p;
  e ≤ N

Tactic:
set e := M.factorization p

Premises used: DFunLike.coe, Nat.factorization
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
p M N : ℕ
inst : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := (M.factorization : (a : ℕ) → ℕ) p
hv : e ≤ N
M' : ℕ := M / p ^ e
⊢ M'.Coprime p

Tactic:
have hM'_cop : M'.Coprime p := (Nat.coprime_ordCompl Fact.out hM).symm
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ Ne (α := ℚ) (↑p : ℚ) 0

Tactic:
have hp_ne : (p : ℚ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.Prime.ne_zero Fact.out)
-- Module: Mathlib.NumberTheory.Bernoulli
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
⊢ p ^ e * M' = M

Tactic:
have hdecomp : p ^ e * M' = M := Nat.ordProj_mul_ordCompl_eq_self M p