awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
this :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 *
      ∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k =
    ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x
rw_mod_cast :
  ∀
    (this :
      HMul.hMul (α := ℚ) (↑(n + 1) : ℚ)
          (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) =
        ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x),
    HMul.hMul (α := ℚ) (↑(n + 1) : ℚ)
          (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) +
        (↑(n + 1) : ℚ) *
          HSub.hSub (α := ℚ) 1 (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) =
      (↑(n + 1) : ℚ)
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli' k) (↑(n + 1) : ℚ)

Tactic:
rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]

Premises used: Nat.choose_succ_self_right, bernoulli'_def, Finset.sum_range_succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
this :
  HMul.hMul (α := ℚ) (↑(n + 1) : ℚ)
      (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) =
    ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x
⊢ HMul.hMul (α := ℚ) (↑(n + 1) : ℚ)
        (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) +
      (↑(n + 1) : ℚ) *
        HSub.hSub (α := ℚ) 1 (∑ x ∈ range n, Rat.divInt (↑(n.choose x) : ℤ) (Int.subNatNat n x + 1) * bernoulli' x) =
    (↑(n + 1) : ℚ)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
succ :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 *
      ∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k =
    ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli' k) (↑(n + 1) : ℚ)

Tactic:
suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
succ :
  Eq (α := ℚ)
    (∑ x ∈ range n,
      HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose x) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑x : ℚ) + 1)) * bernoulli' x)
    (∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x)
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 *
      ∑ k ∈ range n, (↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1) * bernoulli' k =
    ∑ x ∈ range n, (↑(n.succ.choose x) : ℚ) * bernoulli' x

Tactic:
simp_rw [mul_sum, ← mul_assoc]

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

Tactic:
sum_congr rfl fun k hk => ?_

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

Tactic:
refine sum_congr rfl fun k hk => ?_

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

Tactic:
congr
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n k : ℕ
hk : k ∈ range n
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬False
⊢ HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n k : ℕ
hk : k ∈ range n
⊢ HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0

Tactic:
have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n k : ℕ
hk : k ∈ range n
this : HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0
succ :
  (↑(n.choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = (↑((n + 1).choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * ((↑(n.choose k) : ℚ) / (HSub.hSub (α := ℚ) (↑n : ℚ) (↑k : ℚ) + 1)) =
    (↑(n.succ.choose k) : ℚ)

Tactic:
simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]

Premises used: Nat.succ_eq_add_one, Nat.cast_sub, LT.lt.le, Finset.mem_range, Iff.mp, mul_comm
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n k : ℕ
hk : k ∈ range n
this : HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1 ≠ 0
succ succ₁ succ₂ succ₃ succ₄ succ₅ : ∀ (this : ¬False), n.choose k * (n + 1) = (n + 1).choose k * (n - k + 1)
succ₆ : ∀ (this : ¬False), n.choose k * (n + 1) = (n + 1).choose k * (n + 1 - k)
⊢ (↑(n.choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 = (↑((n + 1).choose k) : ℚ) * HAdd.hAdd (α := ℚ) (↑(n - k) : ℚ) 1

Tactic:
rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]

Premises used: Nat.choose_mul_succ_eq, LT.lt.le, Finset.mem_range, tsub_add_eq_add_tsub, Iff.mp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
zero : Eq (α := ℚ) (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) * bernoulli' k) (↑0 : ℚ)
succ : ∀ (n : ℕ), Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli' k) (↑(n + 1) : ℚ)
⊢ Eq (α := ℚ) (∑ k ∈ range n, (↑(n.choose k) : ℚ) * bernoulli' k) (↑n : ℚ)

Tactic:
cases n with | zero => simp | succ n =>
  suffices
    ((n + 1 : ℚ) * ∑ k ∈ range n, ↑(n.choose k) / (n - k + 1) * bernoulli' k) =
      ∑ x ∈ range n, ↑(n.succ.choose x) * bernoulli' x by
    rw_mod_cast [sum_range_succ, bernoulli'_def, ← this, choose_succ_self_right]
    ring
  simp_rw [mul_sum, ← mul_assoc]
  refine sum_congr rfl fun k hk => ?_
  congr
  have : ((n - k : ℕ) : ℚ) + 1 ≠ 0 := by norm_cast
  simp only [← cast_sub (mem_range.1 hk).le, succ_eq_add_one, field, mul_comm]
  rw_mod_cast [tsub_add_eq_add_tsub (mem_range.1 hk).le, choose_mul_succ_eq]

Premises used: Finset.mul_sum, Nat.choose_mul_succ_eq, Nat.succ_eq_add_one, mul_assoc, mul_comm, Nat.zero, Nat.succ, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
h :
  ∀ (n : ℕ),
    Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
      ((coeff n : (a : A⟦X⟧) → A) (X * exp A) : A)
⊢ bernoulli'PowerSeries A * (exp A - 1) = X * exp A

Tactic:
ext n
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff 0 : (a : A⟦X⟧) → A) (X * exp A) : A)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  HMul.hMul (α := A) (β := A)
        ((coeff (n + 1, 0).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
          A)
        ((coeff (n + 1, 0).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
      ∑ p ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := A) (β := A)
          ((coeff (p.1, p.2 + 1).1 : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
            A)
          ((coeff (p.1, p.2 + 1).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
    (coeff (n + 1) : (a : A⟦X⟧) → A) (exp A * X)
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) (X * exp A) : A)

Tactic:
rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']

Premises used: bernoulli'PowerSeries, PowerSeries.X, PowerSeries.coeff_mul, mul_comm, Finset.Nat.sum_antidiagonal_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
this :
  Eq (α := ℚ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
    (↑n ! : ℚ)⁻¹
⊢ HMul.hMul (α := A) (β := A)
        ((coeff (n + 1, 0).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
          A)
        ((coeff (n + 1, 0).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
      ∑ p ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := A) (β := A)
          ((coeff (p.1, p.2 + 1).1 : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
            A)
          ((coeff (p.1, p.2 + 1).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
    (coeff (n + 1) : (a : A⟦X⟧) → A) (exp A * X)

Tactic:
simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this

Premises used: Algebra.algebraMap, Rat, map_sum, congr_arg, Nat.factorial, DFunLike.coe
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  Eq (α := ℚ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
    (↑n ! : ℚ)⁻¹
⊢ HMul.hMul (α := A) (β := A)
        ((coeff (n + 1, 0).1 : (a : A⟦X⟧) → A)
            (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
          A)
        ((coeff (n + 1, 0).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) +
      ∑ p ∈ @antidiagonal _ instAddMonoid _ n,
        HMul.hMul (α := A) (β := A)
          ((coeff (p.1, p.2 + 1).1 : (a : A⟦X⟧) → A)
              (PowerSeries.mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (bernoulli' n / (↑n ! : ℚ))) :
            A)
          ((coeff (p.1, p.2 + 1).2 : (a : A⟦X⟧) → A) (exp A - 1) : A) =
    (coeff (n + 1) : (a : A⟦X⟧) → A) (exp A * X)

Tactic:
suffices (∑ p ∈ antidiagonal n,
      bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
    simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  HMul.hMul (α := ℚ)
      (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
        bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
      (↑n ! : ℚ) =
    1
⊢ Eq (α := ℚ)
    (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
    (↑n ! : ℚ)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Premises used: eq_inv_of_mul_eq_one_left
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  Eq (α := ℚ)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
    1
⊢ HMul.hMul (α := ℚ)
      (∑ p ∈ @antidiagonal _ instAddMonoid _ n,
        bernoulli' p.1 / (↑p.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * (↑p.2! : ℚ))⁻¹)
      (↑n ! : ℚ) =
    1

Tactic:
rw [sum_mul]

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

Tactic:
bernoulli'_spec' n

Premises used: bernoulli'_spec'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  Eq (α := ℚ)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
⊢ Eq (α := ℚ)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
    1

Tactic:
convert! bernoulli'_spec' n using 1

Premises used: bernoulli'_spec'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  ∀ x ∈ @antidiagonal _ instAddMonoid _ n,
    bernoulli' x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n ! : ℚ) =
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1
⊢ Eq (α := ℚ)
    (∑ i ∈ @antidiagonal _ instAddMonoid _ n,
      bernoulli' i.1 / (↑i.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * (↑i.2! : ℚ))⁻¹ * (↑n ! : ℚ))
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  ∀ (x : ℕ × ℕ),
    x.1 + x.2 = n →
      bernoulli' x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n ! : ℚ) =
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1
⊢ ∀ x ∈ @antidiagonal _ instAddMonoid _ n,
    bernoulli' x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n ! : ℚ) =
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1

Tactic:
simp_rw [mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
i j : ℕ
⊢ i ! * j ! ∣ (i + j)!

Tactic:
have := factorial_mul_factorial_dvd_factorial_add i j
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
i j : ℕ
this : i ! * j ! ∣ (i + j)!
⊢ bernoulli' (i, j).1 / (↑(i, j).1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑(i, j).2 : ℚ) 1 * (↑(i, j).2! : ℚ))⁻¹ *
      (↑((i, j).1 + (i, j).2)! : ℚ) =
    (↑(((i, j).1 + (i, j).2).choose (i, j).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(i, j).2 : ℚ) 1 * bernoulli' (i, j).1

Tactic:
simp [field, add_choose, *]

Premises used: Nat.add_choose
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff 0 : (a : A⟦X⟧) → A) (X * exp A) : A)
h₁ :
  ∀ (n : ℕ),
    Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) (X * exp A) : A)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulli'PowerSeries A * (exp A - 1)) : A)
    ((coeff n : (a : A⟦X⟧) → A) (X * exp A) : A)

Tactic:
cases n with | zero => simp | succ n =>
  rw [bernoulli'PowerSeries, coeff_mul, mul_comm X, sum_antidiagonal_succ']
  suffices (∑ p ∈ antidiagonal n,
      bernoulli' p.1 / p.1! * ((p.2 + 1) * p.2! : ℚ)⁻¹) = (n ! : ℚ)⁻¹ by
    simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this
  apply eq_inv_of_mul_eq_one_left
  rw [sum_mul]
  convert! bernoulli'_spec' n using 1
  apply sum_congr rfl
  simp_rw [mem_antidiagonal]
  rintro ⟨i, j⟩ rfl
  have := factorial_mul_factorial_dvd_factorial_add i j
  simp [field, add_choose, *]

Premises used: bernoulli'PowerSeries, eq_inv_of_mul_eq_one_left, PowerSeries.X, bernoulli'_spec', PowerSeries.coeff_mul, Finset.HasAntidiagonal.mem_antidiagonal, mul_comm, Nat.zero, Nat.add_choose, Nat.succ, Finset.sum_congr, rfl, Finset.sum_mul, Finset.Nat.sum_antidiagonal_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
inl : ∀ (h : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) = X), bernoulli' n = 0
inr : ∀ (h : exp ℚ - 1 = 0), bernoulli' n = 0
⊢ bernoulli' n = 0

Tactic:
rcases mul_eq_mul_right_iff.mp this with h | h

Premises used: mul_eq_mul_right_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) = X
⊢ ∀ (n : ℕ),
    Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
      (if n = 1 then 1 else 0 : ℚ)

Tactic:
simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h

Premises used: PowerSeries.evalNegHom, PowerSeries.coeff_X, PowerSeries.ext_iff
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : exp ℚ - 1 = 0
⊢ ∀ (n : ℕ), Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (exp ℚ - 1) : ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) 0 : ℚ)

Tactic:
simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h

Premises used: PowerSeries.evalNegHom, PowerSeries.coeff_X, PowerSeries.ext_iff
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
      (if n = 1 then 1 else 0 : ℚ)
inl : -bernoulli' n = bernoulli' n
⊢ bernoulli' n = 0

Tactic:
apply eq_zero_of_neg_eq

Premises used: eq_zero_of_neg_eq
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  ∀ (n : ℕ),
    Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
      (if n = 1 then 1 else 0 : ℚ)
⊢ Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
    (if n = 1 then 1 else 0 : ℚ)

Tactic:
specialize h n
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h :
  Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
    (if n = 1 then 1 else 0 : ℚ)
pos :
  n = 1 →
    ∀
      (h :
        Eq (α := ℚ)
          ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
          (1 : ℚ)),
      -bernoulli' n = bernoulli' n
neg :
  ¬n = 1 →
    ∀
      (h :
        Eq (α := ℚ)
          ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
          (0 : ℚ)),
      -bernoulli' n = bernoulli' n
⊢ -bernoulli' n = bernoulli' n

Tactic:
split_ifs at h
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h_1 : n = 1
h :
  Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
    (1 : ℚ)
⊢ -bernoulli' n = bernoulli' n

Tactic:
simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]

Premises used: Nat.factorial_ne_zero, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h_1 : ¬n = 1
h :
  Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (HSub.hSub (β := ℚ⟦X⟧) B ((rescale (-1) : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧)) : ℚ)
    (0 : ℚ)
⊢ -bernoulli' n = bernoulli' n

Tactic:
simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]

Premises used: Nat.factorial_ne_zero, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
this : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), Eq (α := ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) (exp ℚ - 1) : ℚ) ((coeff n : (a : ℚ⟦X⟧) → ℚ) 0 : ℚ)
⊢ bernoulli' n = 0

Tactic:
simpa +decide [Nat.factorial] using h 1

Premises used: Nat.factorial, OfNat.ofNat, Decidable.decide
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
suffices : HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)
⊢ bernoulli' n = 0

Tactic:
suffices (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1) by
    rcases mul_eq_mul_right_iff.mp this with h | h <;>
      simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
    · apply eq_zero_of_neg_eq
      specialize h n
      split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]
    · simpa +decide [Nat.factorial] using h 1
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
⊢ B * (exp ℚ - 1) = X * exp ℚ

Tactic:
simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ

Premises used: bernoulli'PowerSeries, Rat, bernoulli'PowerSeries_mul_exp_sub_one
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
⊢ B * (exp ℚ - 1) = X * exp ℚ

Tactic:
have h : B * (exp ℚ - 1) = X * exp ℚ := by
    simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
h : B * (exp ℚ - 1) = X * exp ℚ
rw : HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) (1 - exp ℚ) = -HMul.hMul (α := ℚ⟦X⟧) X 1
⊢ HSub.hSub (β := ℚ⟦X⟧) B ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) * (exp ℚ - 1) = X * (exp ℚ - 1)

Tactic:
rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg]

Premises used: neg_sub, mul_sub, sub_right_inj, neg_eq_iff_eq_neg, PowerSeries.X, sub_mul, mul_neg
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun (n : ℕ) ↦ bernoulli' n / (↑n ! : ℚ)
h : B * (exp ℚ - 1) = X * exp ℚ
this :
  HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) (B * (exp ℚ - 1)) : ℚ⟦X⟧) (exp ℚ) =
    HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) (X * exp ℚ) : ℚ⟦X⟧) (exp ℚ)
⊢ HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) B : ℚ⟦X⟧) (1 - exp ℚ) = -HMul.hMul (α := ℚ⟦X⟧) X 1

Tactic:
simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]

Premises used: PowerSeries.evalNegHom, Rat, mul_assoc, PowerSeries.exp_mul_exp_neg_eq_one, sub_mul, mul_comm, PowerSeries.exp, DFunLike.coe