awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
simp :
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R) *
      HMul.hMul (α := R) (β := R) ((g : (a : ℕ) → R) m : R) ((g : (a : ℕ) → R) n : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((g : (a : ℕ) → R) m : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)
⊢ (f.pmul g : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((f.pmul g : (a : ℕ) → R) m : R) ((f.pmul g : (a : ℕ) → R) n : R)

Tactic:
simp only [pmul_apply, hf.map_mul_of_coprime cop, hg.map_mul_of_coprime cop]

Premises used: ArithmeticFunction.pmul_apply, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f g : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
hg : IsMultiplicative.{u_1} (R := R) g
m n : ℕ
cop : m.Coprime n
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R) *
      HMul.hMul (α := R) (β := R) ((g : (a : ℕ) → R) m : R) ((g : (a : ℕ) → R) n : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((g : (a : ℕ) → R) m : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) ((g : (a : ℕ) → R) n : R)

Tactic:
ring
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
⊢ Eq (α := R) ((f.pdiv g : (a : ℕ) → R) 1 : R) (1 : R)

Tactic:
simp [hf, hg]
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
simp :
  HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R) *
      HMul.hMul (α := R) (β := R) (((g : (a : ℕ) → R) m)⁻¹ : R) (((g : (a : ℕ) → R) n)⁻¹ : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) (((g : (a : ℕ) → R) m)⁻¹ : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (((g : (a : ℕ) → R) n)⁻¹ : R)
⊢ (f.pdiv g : (a : ℕ) → R) (m * n) =
    HMul.hMul (α := R) (β := R) ((f.pdiv g : (a : ℕ) → R) m : R) ((f.pdiv g : (a : ℕ) → R) n : R)

Tactic:
simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop, div_eq_mul_inv,
      mul_inv]

Premises used: mul_inv, div_eq_mul_inv, ArithmeticFunction.pdiv_apply, ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m n : ℕ
cop : m.Coprime n
⊢ HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) ((f : (a : ℕ) → R) n : R) *
      HMul.hMul (α := R) (β := R) (((g : (a : ℕ) → R) m)⁻¹ : R) (((g : (a : ℕ) → R) n)⁻¹ : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) m : R) (((g : (a : ℕ) → R) m)⁻¹ : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : ℕ) → R) n : R) (((g : (a : ℕ) → R) n)⁻¹ : R)

Tactic:
apply mul_mul_mul_comm

Premises used: mul_mul_mul_comm
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
⊢ IsMultiplicative.{u_1} (R := R) (f.ppow 0)

Tactic:
isMultiplicative_zeta.natCast

Premises used: ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.natToArithmeticFunction, ArithmeticFunction.ppow, ArithmeticFunction.isMultiplicative_zeta, dite
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
⊢ IsMultiplicative.{u_1} (R := R) (f.ppow 0)

Tactic:
exact isMultiplicative_zeta.natCast

Premises used: ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.isMultiplicative_zeta
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
k : ℕ
hi : IsMultiplicative.{u_1} (R := R) (f.ppow k)
succ : IsMultiplicative.{u_1} (R := R) (f.pmul (f.ppow k))
⊢ IsMultiplicative.{u_1} (R := R) (f.ppow (k + 1))

Tactic:
rw [ppow_succ']

Premises used: ArithmeticFunction.ppow_succ'
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
k : ℕ
hi : IsMultiplicative.{u_1} (R := R) (f.ppow k)
⊢ IsMultiplicative.{u_1} (R := R) (f.pmul (f.ppow k))

Tactic:
apply hf.pmul hi

Premises used: ArithmeticFunction.IsMultiplicative.pmul
-- Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta
Goal:
R : Type u_1
inst : CommSemiring R
f : ArithmeticFunction R
hf : IsMultiplicative.{u_1} (R := R) f
k : ℕ
zero : IsMultiplicative.{u_1} (R := R) (f.ppow 0)
succ : ∀ (k : ℕ) (hi : IsMultiplicative.{u_1} (R := R) (f.ppow k)), IsMultiplicative.{u_1} (R := R) (f.ppow (k + 1))
⊢ IsMultiplicative.{u_1} (R := R) (f.ppow k)

Tactic:
induction k with
  | zero => exact isMultiplicative_zeta.natCast
  | succ k hi => rw [ppow_succ']; apply hf.pmul hi

Premises used: ArithmeticFunction.zero, ArithmeticFunction.IsMultiplicative.natCast, ArithmeticFunction.ppow_succ', ArithmeticFunction.isMultiplicative_zeta, Nat.succ
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
zero : (↑p : R) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
zero₁ : (↑p : R) ∣ HPow.hPow (β := ℕ) a 1 - HPow.hPow (β := ℕ) b 1
zero₂ : (↑p : R) ∣ a - HPow.hPow (β := ℕ) b 1
zero₃ zero₄ zero₅ zero₆ : (↑p : R) ∣ a - b
⊢ HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 0 1) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0

Tactic:
rwa [pow_one, pow_zero, pow_one, pow_one]

Premises used: pow_zero, pow_one
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
succ :
  (↑p : R) * HPow.hPow (α := R) (↑p : R) (k + 1) ∣
    (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)
⊢ HPow.hPow (α := R) (↑p : R) (k + 1 + 1) ∣ a ^ p ^ (k + 1) - b ^ p ^ (k + 1)

Tactic:
rw [pow_succ p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ']

Premises used: pow_succ, pow_mul, geom_sum₂_mul, pow_succ'
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
⊢ (↑p : R) * HPow.hPow (α := R) (↑p : R) (k + 1) ∣
    (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)

Tactic:
mul_dvd_mul ?_ ih

Premises used: mul_dvd_mul
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
succ : Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i))
⊢ (↑p : R) * HPow.hPow (α := R) (↑p : R) (k + 1) ∣
    (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i)) * (a ^ p ^ k - b ^ p ^ k)

Tactic:
refine mul_dvd_mul ?_ ih

Premises used: mul_dvd_mul
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
r : R
rw : (↑p : R) ∣ r ↔ Membership.mem (γ := Ideal R) (span {(↑p : R)}) r
rw₁ rw₂ : (↑p : R) ∣ r ↔ (↑p : R) ∣ r
⊢ (↑p : R) ∣ r ↔
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
      (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))

Tactic:
rw [eq_zero_iff_mem, mem_span_singleton]

Premises used: Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
⊢ ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))

Tactic:
have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton]
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))

Tactic:
rw [hf, map_sub, sub_eq_zero] at h

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
h₁ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
⊢ ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))

Tactic:
rw [hf, map_sub, sub_eq_zero] at h

Premises used: map_sub, sub_eq_zero
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
h :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
succ : Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) (↑p : R ⧸ span {(↑p : R)}) 0
⊢ Dvd.dvd.{u_1} (α := R) (↑p : R) (∑ i ∈ Finset.range p, (a ^ p ^ k) ^ i * (b ^ p ^ k) ^ (p - 1 - i))

Tactic:
rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]

Premises used: geom_sum₂_self, mul_eq_zero_of_left, map_pow, RingHom.map_geom_sum₂
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
k : ℕ
ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}) := mk (span {(↑p : R)})
h :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) a : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
    ((f : (a : R) → R ⧸ span {(↑p : R)}) b : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
hf :
  ∀ (r : R),
    (↑p : R) ∣ r ↔
      Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        ((f : (a : R) → R ⧸ span {(↑p : R)}) r : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
        (0 : HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)}))
succ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) ((f : (a : R) → R ⧸ span {(↑p : R)}) (↑p : R)) 0
succ₁ : Membership.mem (γ := Ideal R) (span {(↑p : R)}) (↑p : R)
succ₂ succ₃ : Dvd.dvd.{u_1} (α := R) (↑p : R) (↑p : R)
⊢ Eq.{u_1 + 1} (α := HasQuotient.Quotient R (B := Ideal R) (span {(↑p : R)})) (↑p : R ⧸ span {(↑p : R)}) 0

Tactic:
rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]

Premises used: Ideal.Quotient.eq_zero_iff_mem, map_natCast, Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.Basic
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
a b : R
h : (↑p : R) ∣ a - b
k : ℕ
zero : HPow.hPow (α := R) (↑p : R) (HAdd.hAdd (α := ℕ) 0 1) ∣ a ^ HPow.hPow (β := ℕ) p 0 - b ^ HPow.hPow (β := ℕ) p 0
succ :
  ∀ (k : ℕ) (ih : HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k),
    HPow.hPow (α := R) (↑p : R) (k + 1 + 1) ∣ a ^ p ^ (k + 1) - b ^ p ^ (k + 1)
⊢ HPow.hPow (α := R) (↑p : R) (k + 1) ∣ a ^ p ^ k - b ^ p ^ k

Tactic:
induction k with
  | zero => rwa [pow_one, pow_zero, pow_one, pow_one]
  | succ k ih =>
    rw [pow_succ p k, pow_mul, pow_mul, ← geom_sum₂_mul, pow_succ']
    refine mul_dvd_mul ?_ ih
    let f : R →+* R ⧸ span {(p : R)} := mk (span {(p : R)})
    have hf : ∀ r : R, (p : R) ∣ r ↔ f r = 0 := fun r ↦ by rw [eq_zero_iff_mem, mem_span_singleton]
    rw [hf, map_sub, sub_eq_zero] at h
    rw [hf, RingHom.map_geom_sum₂, map_pow, map_pow, h, geom_sum₂_self, mul_eq_zero_of_left]
    rw [← map_natCast f, eq_zero_iff_mem, mem_span_singleton]

Premises used: geom_sum₂_self, map_sub, sub_eq_zero, pow_succ, mul_eq_zero_of_left, map_pow, pow_mul, Ideal.Quotient.eq_zero_iff_mem, pow_zero, pow_one, geom_sum₂_mul, RingHom.map_geom_sum₂, Ideal.mem_span_singleton, pow_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
rw rw₁ :
  HSub.hSub (α := ℚ) 1
      (∑ k : Fin n,
        (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ)) =
    HSub.hSub (α := ℚ) 1
      (∑ k : Fin n,
        (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ))
⊢ bernoulli' n =
    HSub.hSub (α := ℚ) 1
      (∑ k : Fin n,
        (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ))

Tactic:
rw [bernoulli']

Premises used: bernoulli'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
rw :
  HSub.hSub (α := ℚ) 1
      (∑ k : Fin n,
        (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ)) =
    HSub.hSub (α := ℚ) 1
      (∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
rw₁ rw₂ :
  HSub.hSub (α := ℚ) 1
      (∑ k : Fin n,
        (↑(n.choose (↑k : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑k : ℕ) : ℚ) + 1) * bernoulli' (↑k : ℕ)) =
    HSub.hSub (α := ℚ) 1
      (∑ i : Fin n,
        (↑(n.choose (↑i : ℕ)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑(↑i : ℕ) : ℚ) + 1) * bernoulli' (↑i : ℕ))
⊢ bernoulli' n =
    HSub.hSub (α := ℚ) 1
      (∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)

Tactic:
rw [bernoulli'_def', ← Fin.sum_univ_eq_sum_range]

Premises used: Fin.sum_univ_eq_sum_range, bernoulli'_def'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
rw :
  Eq (α := ℚ)
    (∑ x ∈ range n,
      ((↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
        (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x))
    0
⊢ Eq (α := ℚ)
    (∑ k ∈ range n.succ, (↑(n.choose (n - k)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k) 1

Tactic:
rw [sum_range_succ_comm, bernoulli'_def n, tsub_self, choose_zero_right, sub_self, zero_add,
    div_one, cast_one, one_mul, sub_add, ← sum_sub_distrib, ← sub_eq_zero, sub_sub_cancel_left,
    neg_eq_zero]

Premises used: sub_add, sub_self, sub_eq_zero, tsub_self, Finset.sum_range_succ_comm, neg_eq_zero, sub_sub_cancel_left, zero_add, Finset.sum_sub_distrib, bernoulli'_def, div_one, Nat.cast_one, Nat.choose_zero_right, one_mul
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n x : ℕ
hx : x ∈ range n
rw :
  (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
      (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x =
    0
rw₁ rw₂ : Eq (α := ℚ) 0 0
⊢ (↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
      (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x =
    0

Tactic:
rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self]

Premises used: sub_self, le_of_lt, Finset.mem_range, Nat.choose_symm, Iff.mp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ x ∈ range n,
      ((↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x -
        (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x))
    0

Tactic:
exact Finset.sum_eq_zero (fun x hx => by rw [choose_symm (le_of_lt (mem_range.1 hx)), sub_self])

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
    1

Tactic:
((sum_antidiagonal_eq_sum_range_succ_mk _ n).trans ?_).trans (bernoulli'_spec n)

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, bernoulli'_spec, Eq.trans
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
refine :
  Eq (α := ℚ)
    (∑ k ∈ range n.succ,
      (↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(k, n - k).2 : ℚ) 1 *
        bernoulli' (k, n - k).1)
    (∑ k ∈ range n.succ, (↑(n.choose (n - k)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
    1

Tactic:
refine ((sum_antidiagonal_eq_sum_range_succ_mk _ n).trans ?_).trans (bernoulli'_spec n)

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, bernoulli'_spec, Eq.trans
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
⊢ Eq (α := ℚ)
    (∑ k ∈ range n.succ,
      (↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(k, n - k).2 : ℚ) 1 *
        bernoulli' (k, n - k).1)
    (∑ k ∈ range n.succ, (↑(n.choose (n - k)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)

Tactic:
sum_congr rfl fun x hx => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
refine :
  ∀ (x : ℕ) (hx : x ∈ range n.succ),
    (↑(((x, n - x).1 + (x, n - x).2).choose (x, n - x).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(x, n - x).2 : ℚ) 1 *
        bernoulli' (x, n - x).1 =
      (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x
⊢ Eq (α := ℚ)
    (∑ k ∈ range n.succ,
      (↑(((k, n - k).1 + (k, n - k).2).choose (k, n - k).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(k, n - k).2 : ℚ) 1 *
        bernoulli' (k, n - k).1)
    (∑ k ∈ range n.succ, (↑(n.choose (n - k)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k)

Tactic:
refine sum_congr rfl fun x hx => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n x : ℕ
hx : x ∈ range n.succ
⊢ (↑(((x, n - x).1 + (x, n - x).2).choose (x, n - x).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(x, n - x).2 : ℚ) 1 *
      bernoulli' (x, n - x).1 =
    (↑(n.choose (n - x)) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1) * bernoulli' x

Tactic:
simp only [add_tsub_cancel_of_le, mem_range_succ_iff.mp hx, cast_sub]

Premises used: Nat.cast_sub, Finset.mem_range_succ_iff, Iff.mp, add_tsub_cancel_of_le
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
rw :
  HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) / (HSub.hSub (α := ℚ) (↑0 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    1
⊢ bernoulli' 0 = 1

Tactic:
rw [bernoulli'_def]

Premises used: bernoulli'_def
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) / (HSub.hSub (α := ℚ) (↑0 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
rw :
  HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 1, (↑(Nat.choose 1 k) : ℚ) / (HSub.hSub (α := ℚ) (↑1 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    1 / 2
⊢ bernoulli' 1 = 1 / 2

Tactic:
rw [bernoulli'_def]

Premises used: bernoulli'_def
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 1, (↑(Nat.choose 1 k) : ℚ) / (HSub.hSub (α := ℚ) (↑1 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    1 / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
rw :
  HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 2, (↑(Nat.choose 2 k) : ℚ) / (HSub.hSub (α := ℚ) (↑2 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    1 / 6
⊢ bernoulli' 2 = 1 / 6

Tactic:
rw [bernoulli'_def]

Premises used: bernoulli'_def
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 2, (↑(Nat.choose 2 k) : ℚ) / (HSub.hSub (α := ℚ) (↑2 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    1 / 6

Tactic:
norm_num [sum_range_succ, sum_range_succ, sum_range_zero]

Premises used: Finset.sum_range_zero, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
rw :
  HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 3, (↑(Nat.choose 3 k) : ℚ) / (HSub.hSub (α := ℚ) (↑3 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    0
⊢ bernoulli' 3 = 0

Tactic:
rw [bernoulli'_def]

Premises used: bernoulli'_def
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 3, (↑(Nat.choose 3 k) : ℚ) / (HSub.hSub (α := ℚ) (↑3 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    0

Tactic:
norm_num [sum_range_succ, sum_range_succ, sum_range_zero]

Premises used: Finset.sum_range_zero, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ Nat.choose 4 2 = 6

Tactic:
decide
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ Nat.choose 4 2 = 6

Tactic:
have : Nat.choose 4 2 = 6 := by decide
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
this : Nat.choose 4 2 = 6
rw :
  HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 4, (↑(Nat.choose 4 k) : ℚ) / (HSub.hSub (α := ℚ) (↑4 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    -1 / 30
⊢ bernoulli' 4 = -1 / 30

Tactic:
rw [bernoulli'_def]

Premises used: bernoulli'_def
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
this : Nat.choose 4 2 = 6
⊢ HSub.hSub (α := ℚ) 1
      (∑ k ∈ range 4, (↑(Nat.choose 4 k) : ℚ) / (HSub.hSub (α := ℚ) (↑4 : ℚ) (↑k : ℚ) + 1) * bernoulli' k) =
    -1 / 30

Tactic:
norm_num [sum_range_succ, sum_range_succ, sum_range_zero, this]

Premises used: Finset.sum_range_zero, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ Eq (α := ℚ) (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) * bernoulli' k) (↑0 : ℚ)

Tactic:
simp