awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
h : (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = val (n := p) 0
⊢ False

Tactic:
apply Units.ne_zero a (val_injective p h)

Premises used: ZMod.val_injective, Units.ne_zero
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
⊢ (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p

Tactic:
val_lt _

Premises used: ZMod.val_lt
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
⊢ (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha < p

Tactic:
exact val_lt _

Premises used: ZMod.val_lt
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a₁ : (ZMod p)ˣ
refine_2 :
  ∀ (ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁) (a₂ : (ZMod p)ˣ)
    (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂
⊢ ∀ (ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁) (a₂ : (ZMod p)ˣ)
    (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a₁ : (ZMod p)ˣ
ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁
refine_2 :
  ∀ (a₂ : (ZMod p)ˣ) (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂
⊢ ∀ (a₂ : (ZMod p)ˣ) (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a₁ : (ZMod p)ˣ
ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁
a₂ : (ZMod p)ˣ
refine_2 :
  ∀ (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂
⊢ ∀ (ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂),
    Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
        ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂) →
      a₁ = a₂

Tactic:
_
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a₁ : (ZMod p)ˣ
ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁
a₂ : (ZMod p)ˣ
ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂
h :
  Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
    ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂)
refine_2 : (↑a₁ : ZMod p) = (↑a₂ : ZMod p)
⊢ a₁ = a₂

Tactic:
rw [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a₁ : (ZMod p)ˣ
ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁
a₂ : (ZMod p)ˣ
ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂
h :
  Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
    ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂)
⊢ (↑a₁ : ZMod p) = (↑a₂ : ZMod p)

Tactic:
val_injective p h

Premises used: ZMod.val_injective
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a₁ : (ZMod p)ˣ
ha₁ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₁
a₂ : (ZMod p)ˣ
ha₂ : Membership.mem (γ := Finset (ZMod p)ˣ) univ a₂
h :
  Eq (α := ℕ) ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₁ ha₁)
    ((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a₂ ha₂)
⊢ (↑a₁ : ZMod p) = (↑a₂ : ZMod p)

Tactic:
exact val_injective p h

Premises used: ZMod.val_injective
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ∈ Ico 1 (p - 1).succ
⊢ b ≠ 0 ∧ b < p

Tactic:
rw [mem_Ico, Nat.succ_le_iff, ← succ_sub hp, Nat.add_one_sub_one, pos_iff_ne_zero] at hb

Premises used: Nat.add_one_sub_one, Nat.succ_sub, Nat.succ_le_iff, pos_iff_ne_zero, Finset.mem_Ico
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b

Tactic:
⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩

Premises used: Finset.mem_univ, Nat.cast, Units.mk0, Exists.intro
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
refine_3 : Ne (α := ZMod p) (↑b : ZMod p) 0
refine_3₁ :
  (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val)
      (Units.mk0 (↑b : ZMod p) ⋯) ⋯ =
    b
⊢ ∃ (a : (ZMod p)ˣ) (ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a),
    (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha = b

Tactic:
refine ⟨Units.mk0 b ?_, Finset.mem_univ _, ?_⟩
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : Eq (α := ZMod p) (↑b : ZMod p) 0
refine_3 : b = 0
⊢ False

Tactic:
apply hb.1

Premises used: And.left
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : Eq (α := ZMod p) (↑b : ZMod p) 0
⊢ val (n := p) (↑b : ZMod p) = val (n := p) 0

Tactic:
apply_fun val at h

Premises used: ZMod.val
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
h : val (n := p) (↑b : ZMod p) = val (n := p) 0
⊢ b = 0

Tactic:
simpa only [val_cast_of_lt hb.right, val_zero] using h

Premises used: ZMod.val_cast_of_lt, ZMod.val_zero, And.right
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ (fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val)
      (Units.mk0 (↑b : ZMod p) ⋯) ⋯ =
    b

Tactic:
simp only [val_cast_of_lt hb.right, Units.val_mk0]

Premises used: ZMod.val_cast_of_lt, And.right, Units.val_mk0
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : Membership.mem (γ := Finset (ZMod p)ˣ) univ a
⊢ (↑a : ZMod p) =
    (↑((fun (a : (ZMod p)ˣ) (x : Membership.mem (γ := Finset (ZMod p)ˣ) univ a) ↦ (↑a : ZMod p).val) a ha) : ZMod p)

Tactic:
simp only [cast_id, natCast_val]

Premises used: ZMod.natCast_val, ZMod.cast_id
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ∏ x ∈ Ico 1 p, (↑x : ZMod p)
a₁ : -1
| Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)

Tactic:
congr
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : Ico 1 p
a₁ : fun (x : ℕ) ↦ (↑x : ZMod p)
| ∏ x ∈ Ico 1 p, (↑x : ZMod p)

Tactic:
congr
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : Ico 1 (p - succ 0).succ
| Ico 1 p

Tactic:
rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]

Premises used: Nat.add_one_sub_one, Nat.Prime.pos, Nat.succ_sub, Fact.out
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : Ico 1 (p - succ 0).succ
a₁ : fun (x : ℕ) ↦ (↑x : ZMod p)
a₂ : -1
| Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)

Tactic:
congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]

Premises used: Nat.add_one_sub_one, Nat.Prime.pos, Nat.succ_sub, Fact.out
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
conv : Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - succ 0).succ, (↑x : ZMod p)) (-1)
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 p, (↑x : ZMod p)) (-1)

Tactic:
conv =>
    congr
    congr
    rw [← Nat.add_one_sub_one p, succ_sub (Fact.out (p := p.Prime)).pos]

Premises used: Nat.add_one_sub_one, Nat.Prime.pos, Nat.succ_sub, Fact.out
-- Module: Mathlib.NumberTheory.Wilson
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
rw : Eq (α := ZMod p) (↑(∏ i ∈ Ico 1 (p - succ 0).succ, i) : ZMod p) (-1)
rw₁ : Eq (α := ZMod p) (↑(p - succ 0)! : ZMod p) (-1)
rw₂ rw₃ : Eq (α := ZMod p) (-1) (-1)
⊢ Eq (α := ZMod p) (∏ x ∈ Ico 1 (p - succ 0).succ, (↑x : ZMod p)) (-1)

Tactic:
rw [← prod_natCast, Finset.prod_Ico_id_eq_factorial, wilsons_lemma]

Premises used: ZMod.wilsons_lemma, Finset.prod_Ico_id_eq_factorial, Finset.prod_natCast
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h1 : n ≠ 1
inl : ∀ (h : Eq (α := ZMod 0) (↑(HSub.hSub (α := ℕ) 0 1)! : ZMod 0) (-1)) (h1 : Ne (α := ℕ) 0 1), Prime 0
inr : ∀ (h0 : n ≠ 0), Prime n
⊢ Prime n

Tactic:
rcases eq_or_ne n 0 with (rfl | h0)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Wilson
Goal:
h : Eq (α := ZMod 0) (↑(HSub.hSub (α := ℕ) 0 1)! : ZMod 0) (-1)
h1 : Ne (α := ℕ) 0 1
⊢ Prime 0

Tactic:
norm_num at h
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h1 : n ≠ 1
h0 : n ≠ 0
⊢ 1 < n

Tactic:
replace h1 : 1 < n := n.two_le_iff.mpr ⟨h0, h1⟩
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
inr : ∀ (h2 : ¬Prime n), False
⊢ Prime n

Tactic:
by_contra h2
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
inr : ∀ (m : ℕ) (hm1 : m ∣ n) (hm2 : 1 < m) (hm3 : m < n), False
⊢ False

Tactic:
obtain ⟨m, hm1, hm2 : 1 < m, hm3⟩ := exists_dvd_of_not_prime2 h1 h2

Premises used: Nat.exists_dvd_of_not_prime2
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
⊢ m ∣ (n - 1)!

Tactic:
have hm : m ∣ (n - 1)! := Nat.dvd_factorial (pos_of_gt hm2) (le_pred_of_lt hm3)
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
⊢ False

Tactic:
hm2.ne' (Nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans ?_)))

Premises used: Nat.dvd_add_right, Nat.dvd_one, LT.lt.ne', Iff.mp, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
inr : n ∣ (n - 1)! + 1
⊢ False

Tactic:
refine hm2.ne' (Nat.dvd_one.mp ((Nat.dvd_add_right hm).mp (hm1.trans ?_)))

Premises used: Nat.dvd_add_right, Nat.dvd_one, LT.lt.ne', Iff.mp, Dvd.dvd.trans
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
m : ℕ
hm1 : m ∣ n
hm2 : 1 < m
hm3 : m < n
hm : m ∣ (n - 1)!
inr : Eq (α := ZMod n) (↑((n - 1)! + 1) : ZMod n) 0
inr₁ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) (↑1 : ZMod n) = 0
inr₂ : HAdd.hAdd (α := ZMod n) (↑(n - 1)! : ZMod n) 1 = 0
inr₃ : HAdd.hAdd (α := ZMod n) (-1) 1 = 0
inr₄ inr₅ : Eq (α := ZMod n) 0 0
⊢ n ∣ (n - 1)! + 1

Tactic:
rw [← ZMod.natCast_eq_zero_iff, cast_add, cast_one, h, neg_add_cancel]

Premises used: ZMod.natCast_eq_zero_iff, Nat.cast_add, neg_add_cancel, Nat.cast_one
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : n ≠ 1
⊢ Prime n ↔ Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)

Tactic:
⟨fun h1 => ?_, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩

Premises used: Iff.intro, Nat.prime_of_fac_equiv_neg_one
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : n ≠ 1
refine : ∀ (h1 : Prime n), Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)
⊢ Prime n ↔ Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)

Tactic:
refine ⟨fun h1 => ?_, fun h2 => prime_of_fac_equiv_neg_one h2 h⟩
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : n ≠ 1
h1 : Prime n
⊢ Fact (Prime n)

Tactic:
haveI := Fact.mk h1
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : n ≠ 1
h1 : Prime n
this : Fact (Prime n)
⊢ Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)

Tactic:
ZMod.wilsons_lemma n

Premises used: ZMod.wilsons_lemma
-- Module: Mathlib.NumberTheory.Wilson
Goal:
n : ℕ
h : n ≠ 1
h1 : Prime n
this : Fact (Prime n)
⊢ Eq (α := ZMod n) (↑(n - 1)! : ZMod n) (-1)

Tactic:
exact ZMod.wilsons_lemma n

Premises used: ZMod.wilsons_lemma
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
x : ℝ
⊢ bernoulliFun 0 x = 1

Tactic:
simp only [bernoulliFun, Polynomial.bernoulli_zero, Polynomial.map_one, Polynomial.eval_one]

Premises used: Polynomial.map_one, Polynomial.bernoulli_zero, bernoulliFun, Polynomial.eval_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
x : ℝ
simp : HDiv.hDiv (α := ℝ) (-1) 2 + x = x - 2⁻¹
⊢ bernoulliFun 1 x = x - 1 / 2

Tactic:
simp [bernoulliFun, Polynomial.bernoulli_def, Finset.sum_range_succ]

Premises used: bernoulliFun, Polynomial.bernoulli_def, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
x : ℝ
⊢ HDiv.hDiv (α := ℝ) (-1) 2 + x = x - 2⁻¹

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
x : ℝ
simp : 6⁻¹ + -x + HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℕ) x 2 - x + 6⁻¹
⊢ bernoulliFun 2 x = HPow.hPow (β := ℕ) x 2 - x + 6⁻¹

Tactic:
simp [bernoulliFun, Polynomial.bernoulli_def, Finset.sum_range_succ]

Premises used: bernoulliFun, Polynomial.bernoulli_def, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
x : ℝ
⊢ 6⁻¹ + -x + HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℕ) x 2 - x + 6⁻¹

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
rw : Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
rw₁ :
  Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (Polynomial.eval 0 (Polynomial.bernoulli k)) : ℝ)
    ((↑(bernoulli k) : ℝ) : ℝ)
rw₂ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli k) : ℝ) ((↑(bernoulli k) : ℝ) : ℝ)
rw₃ rw₄ : Eq (α := ℝ) (↑(bernoulli k) : ℝ) (↑(bernoulli k) : ℝ)
⊢ bernoulliFun k 0 = (↑(bernoulli k) : ℝ)

Tactic:
rw [bernoulliFun, Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]

Premises used: Polynomial.bernoulli_eval_zero, bernoulliFun, Polynomial.eval_zero_map, eq_ratCast
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 1
rw : bernoulliFun k 1 = (↑(bernoulli k) : ℝ)
rw₁ : Polynomial.eval 1 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)) = (↑(bernoulli k) : ℝ)
rw₂ :
  Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (Polynomial.eval 1 (Polynomial.bernoulli k)) : ℝ)
    ((↑(bernoulli k) : ℝ) : ℝ)
rw₃ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) : ℝ) ((↑(bernoulli k) : ℝ) : ℝ)
rw₄ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) : ℝ) ((↑(bernoulli' k) : ℝ) : ℝ)
rw₅ rw₆ : Eq (α := ℝ) (↑(bernoulli' k) : ℝ) (↑(bernoulli' k) : ℝ)
⊢ bernoulliFun k 1 = bernoulliFun k 0

Tactic:
rw [bernoulliFun_eval_zero, bernoulliFun, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one,
    bernoulli_eq_bernoulli'_of_ne_one hk, eq_ratCast]

Premises used: Polynomial.bernoulli_eval_one, bernoulliFun, Polynomial.eval_one_map, bernoulliFun_eval_zero, eq_ratCast, bernoulli_eq_bernoulli'_of_ne_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
rw : (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) = HAdd.hAdd (α := ℝ) (↑(bernoulli k) : ℝ) (if k = 1 then 1 else 0)
⊢ bernoulliFun k 1 = bernoulliFun k 0 + if k = 1 then 1 else 0

Tactic:
rw [bernoulliFun, bernoulliFun_eval_zero, Polynomial.eval_one_map, Polynomial.bernoulli_eval_one]

Premises used: Polynomial.bernoulli_eval_one, bernoulliFun, Polynomial.eval_one_map, bernoulliFun_eval_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
pos : ∀ (h : k = 1), (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) = HAdd.hAdd (α := ℝ) (↑(bernoulli k) : ℝ) 1
neg : ∀ (h : ¬k = 1), (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) = HAdd.hAdd (α := ℝ) (↑(bernoulli k) : ℝ) 0
⊢ (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) = HAdd.hAdd (α := ℝ) (↑(bernoulli k) : ℝ) (if k = 1 then 1 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
h : k = 1
pos : (↑(1 / 2) : ℝ) = HAdd.hAdd (α := ℝ) (↑(-1 / 2) : ℝ) 1
⊢ (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) = HAdd.hAdd (α := ℝ) (↑(bernoulli k) : ℝ) 1

Tactic:
rw [h, bernoulli_one, bernoulli'_one, eq_ratCast]

Premises used: eq_ratCast, bernoulli'_one, bernoulli_one
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
h : k = 1
pos : HDiv.hDiv (α := ℝ) 1 2 = HDiv.hDiv (α := ℝ) (-1) 2 + 1
⊢ (↑(1 / 2) : ℝ) = HAdd.hAdd (α := ℝ) (↑(-1 / 2) : ℝ) 1

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
h : k = 1
⊢ HDiv.hDiv (α := ℝ) 1 2 = HDiv.hDiv (α := ℝ) (-1) 2 + 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
h : ¬k = 1
neg : (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) = HAdd.hAdd (α := ℝ) (↑(bernoulli' k) : ℝ) 0
neg₁ : Eq (α := ℝ) ((algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) : ℝ) ((↑(bernoulli' k) : ℝ) : ℝ)
neg₂ neg₃ : Eq (α := ℝ) (↑(bernoulli' k) : ℝ) (↑(bernoulli' k) : ℝ)
⊢ (algebraMap ℚ ℝ : (a : ℚ) → ℝ) (bernoulli' k) = HAdd.hAdd (α := ℝ) (↑(bernoulli k) : ℝ) 0

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one h, add_zero, eq_ratCast]

Premises used: eq_ratCast, bernoulli_eq_bernoulli'_of_ne_one, add_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))
    (Polynomial.eval x
      ((Polynomial.derivative : (a : Polynomial ℝ) → Polynomial ℝ)
        (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k))))
    x

Tactic:
((Polynomial.bernoulli k).map <| algebraMap ℚ ℝ).hasDerivAt x

Premises used: Real, Algebra.algebraMap, Polynomial.bernoulli, Rat, Polynomial.hasDerivAt, Polynomial.map
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
h :
  (↑k : ℝ) * bernoulliFun (k - 1) x =
    Polynomial.eval x
      ((Polynomial.derivative : (a : Polynomial ℝ) → Polynomial ℝ)
        (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))
⊢ HasDerivAt (bernoulliFun k) ((↑k : ℝ) * bernoulliFun (k - 1) x) x

Tactic:
convert! ((Polynomial.bernoulli k).map <| algebraMap ℚ ℝ).hasDerivAt x using 1

Premises used: Real, Algebra.algebraMap, Polynomial.bernoulli, Rat, Polynomial.hasDerivAt, Polynomial.map
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
⊢ (↑k : ℝ) * bernoulliFun (k - 1) x =
    Polynomial.eval x
      ((Polynomial.derivative : (a : Polynomial ℝ) → Polynomial ℝ)
        (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli k)))

Tactic:
simp only [bernoulliFun, Polynomial.derivative_map, Polynomial.derivative_bernoulli k,
    Polynomial.map_mul, Polynomial.map_natCast, Polynomial.eval_mul, Polynomial.eval_natCast]

Premises used: Polynomial.map_mul, Polynomial.eval_natCast, bernoulliFun, Polynomial.eval_mul, Polynomial.derivative_map, Polynomial.derivative_bernoulli, Polynomial.map_natCast
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
⊢ ContDiff ℝ ⊤ (bernoulliFun k)

Tactic:
simp +unfoldPartialApp [bernoulliFun, Polynomial.eval_map_algebraMap, Polynomial.contDiff_aeval]

Premises used: bernoulliFun, Polynomial.contDiff_aeval, Polynomial.eval_map_algebraMap
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
⊢ Continuous (bernoulliFun k)

Tactic:
Polynomial.continuous_aeval _

Premises used: Polynomial.eval, Polynomial.continuous_aeval, MonoidHomClass.toMonoidHom, bernoulliFun, RingHomClass.toRingHom
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
a b : ℝ
⊢ IntervalIntegrable (bernoulliFun k) volume a b

Tactic:
(continuous_bernoulliFun k).intervalIntegrable a b

Premises used: Continuous.intervalIntegrable, continuous_bernoulliFun
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
h : ∀ (x : ℝ), deriv (bernoulliFun k) x = (↑k : ℝ) * bernoulliFun (k - 1) x
⊢ deriv (bernoulliFun k) = fun (x : ℝ) ↦ (↑k : ℝ) * bernoulliFun (k - 1) x

Tactic:
ext x
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
⊢ deriv (bernoulliFun k) x = (↑k : ℝ) * bernoulliFun (k - 1) x

Tactic:
(hasDerivAt_bernoulliFun _ _).deriv

Premises used: hasDerivAt_bernoulliFun, HasDerivAt.deriv
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
⊢ deriv (bernoulliFun k) x = (↑k : ℝ) * bernoulliFun (k - 1) x

Tactic:
exact (hasDerivAt_bernoulliFun _ _).deriv

Premises used: hasDerivAt_bernoulliFun, HasDerivAt.deriv
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ bernoulliFun (k + 1) x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
    ((↑(k + 1) : ℝ) * bernoulliFun (k + 1 - 1) x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) x

Tactic:
(hasDerivAt_bernoulliFun (k + 1) x).div_const _

Premises used: hasDerivAt_bernoulliFun, HAdd.hAdd, HasDerivAt.div_const, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
h : bernoulliFun k x = (↑(k + 1) : ℝ) * bernoulliFun (k + 1 - 1) x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ HasDerivAt (fun (x : ℝ) ↦ bernoulliFun (k + 1) x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) (bernoulliFun k x) x

Tactic:
convert! (hasDerivAt_bernoulliFun (k + 1) x).div_const _ using 1

Premises used: hasDerivAt_bernoulliFun, HAdd.hAdd, HasDerivAt.div_const, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x : ℝ
⊢ bernoulliFun k x = (↑(k + 1) : ℝ) * bernoulliFun (k + 1 - 1) x / HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
simp [Nat.cast_add_one_ne_zero k]

Premises used: Nat.cast_add_one_ne_zero
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..1, bernoulliFun k x) (if k = 0 then 1 else 0)

Tactic:
simp +contextual [integral_eq_sub_of_hasDerivAt (fun x _ => antideriv_bernoulliFun k x)
      (intervalIntegrable_bernoulliFun k _ _), bernoulliFun_eval_one, ← sub_div, ite_div]

Premises used: intervalIntegrable_bernoulliFun, antideriv_bernoulliFun, bernoulliFun_eval_one, ite_div, sub_div, intervalIntegral.integral_eq_sub_of_hasDerivAt
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
hk : k ≠ 0
rw : Eq (α := ℝ) (if k = 0 then 1 else 0) 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ) (∫ (x : ℝ) in 0..1, bernoulliFun k x) 0

Tactic:
rw [integral_bernoulliFun, if_neg hk]

Premises used: integral_bernoulliFun, if_neg
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x y : ℝ
hderiv : ∀ x_1 ∈ [[x, y]], HasDerivAt (bernoulliFun (k + 1)) ((↑(k + 1) : ℝ) * bernoulliFun k x_1) x_1
hint : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ (↑(k + 1) : ℝ) * bernoulliFun k t) volume x y
⊢ bernoulliFun (k + 1) y = bernoulliFun (k + 1) x + ∫ (t : ℝ) in x..y, (↑(k + 1) : ℝ) * bernoulliFun k t

Tactic:
rw [intervalIntegral.integral_eq_sub_of_hasDerivAt, add_sub_cancel]

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt, add_sub_cancel
-- Module: Mathlib.NumberTheory.ZetaValues
Goal:
k : ℕ
x y : ℝ
⊢ ∀ x_1 ∈ [[x, y]], HasDerivAt (bernoulliFun (k + 1)) ((↑(k + 1) : ℝ) * bernoulliFun k x_1) x_1

Tactic:
fun y _ ↦ hasDerivAt_bernoulliFun _ y

Premises used: hasDerivAt_bernoulliFun, HAdd.hAdd, OfNat.ofNat, Nat.pred