awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
H :
  (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1 +
      ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1 =
    1
p : ℕ × ℕ
h : p ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)}
h' : p ∈ @antidiagonal _ instAddMonoid _ n.succ
h'' : p ≠ (1, n)
⊢ (↑((p.1 + p.2).choose p.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * bernoulli p.1 =
    (↑((p.1 + p.2).choose p.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑p.2 : ℚ) 1 * bernoulli' p.1

Tactic:
simp [bernoulli_eq_bernoulli'_of_ne_one ((not_congr (antidiagonal_congr h' h₁)).mp h'')]

Premises used: Finset.antidiagonal_congr, Iff.mp, bernoulli_eq_bernoulli'_of_ne_one, not_congr
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
H :
  (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1 +
      ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1 =
    1
h : 1 = HSub.hSub (α := ℚ) 2 1
⊢ 0 - (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli (1, n).1 =
    1 - (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1

Tactic:
simp [field, h₃]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
H :
  (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1 +
      ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
        (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1 =
    1
⊢ 1 = HSub.hSub (α := ℚ) 2 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
zero :
  Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ 0,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
    (if Eq (α := ℕ) 0 0 then 1 else 0)
succ :
  ∀ (n : ℕ),
    Eq (α := ℚ)
      (∑ k ∈ @antidiagonal _ instAddMonoid _ (n + 1),
        (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
      (if n + 1 = 0 then 1 else 0)
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
    (if n = 0 then 1 else 0)

Tactic:
cases n with | zero => simp | succ n =>
  rw [if_neg (succ_ne_zero _)]
  -- algebra facts
  have h₁ : (1, n) ∈ antidiagonal n.succ := by simp [mem_antidiagonal, add_comm]
  have h₃ : (1 + n).choose n = n + 1 := by simp [add_comm]
  -- key equation: the corresponding fact for `bernoulli'`
  have H := bernoulli'_spec' n.succ
  -- massage it to match the structure of the goal, then convert piece by piece
  rw [sum_eq_add_sum_diff_singleton_of_mem h₁] at H ⊢
  apply add_eq_of_eq_sub'
  convert! eq_sub_of_add_eq' H using 1
  · refine sum_congr rfl fun p h => ?_
    obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h
    simp [bernoulli_eq_bernoulli'_of_ne_one ((not_congr (antidiagonal_congr h' h₁)).mp h'')]
  · simp [field, h₃]
    norm_num

Premises used: Nat.succ_ne_zero, Nat.zero, add_eq_of_eq_sub', Nat.succ, if_neg, 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) (bernoulliPowerSeries A * (exp A - 1)) : A)
      ((coeff n : (a : A⟦X⟧) → A) X : A)
⊢ bernoulliPowerSeries A * (exp A - 1) = X

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) (bernoulliPowerSeries A * (exp A - 1)) : A) ((coeff 0 : (a : A⟦X⟧) → A) X : A)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  HAdd.hAdd (β := A)
      (HMul.hMul (α := A)
        ((algebraMap ℚ A : (a : ℚ) → A) (bernoulli (n + 1) / (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (↑n ! : ℚ))) : A)
        (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
      ((algebraMap ℚ A : (a : ℚ) → A)
          (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
            bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
        A) =
    if n + 1 = 1 then 1 else 0
⊢ Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (bernoulliPowerSeries A * (exp A - 1)) : A)
    ((coeff (n + 1) : (a : A⟦X⟧) → A) X : A)

Tactic:
simp only [bernoulliPowerSeries, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk,
    coeff_one, coeff_exp, map_sub, factorial, if_pos, cast_succ, cast_mul,
    sub_zero, add_eq_zero, if_false, one_ne_zero, and_false, ← map_mul, ← map_sum]

Premises used: Nat.cast_succ, map_sub, sub_zero, if_false, PowerSeries.coeff_mk, PowerSeries.coeff_exp, if_pos, map_sum, PowerSeries.coeff_mul, map_mul, PowerSeries.coeff_X, Nat.cast_mul, Nat.factorial, PowerSeries.coeff_one, one_div, and_false, add_eq_zero, one_ne_zero, bernoulliPowerSeries, Finset.Nat.sum_antidiagonal_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ HAdd.hAdd (β := A)
      (HMul.hMul (α := A)
        ((algebraMap ℚ A : (a : ℚ) → A)
            (bernoulli (HAdd.hAdd (α := ℕ) 0 1) / (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1 * (↑0! : ℚ))) :
          A)
        (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
      ((algebraMap ℚ A : (a : ℚ) → A)
          (∑ x ∈ @antidiagonal _ instAddMonoid _ 0,
            bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
        A) =
    if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  HAdd.hAdd (β := A)
      (HMul.hMul (α := A)
        ((algebraMap ℚ A : (a : ℚ) → A)
            (bernoulli (n + 1 + 1) / (HAdd.hAdd (α := ℚ) (↑(n + 1) : ℚ) 1 * (↑(n + 1)! : ℚ))) :
          A)
        (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
      ((algebraMap ℚ A : (a : ℚ) → A)
          (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
            bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
        A) =
    0
⊢ HAdd.hAdd (β := A)
      (HMul.hMul (α := A)
        ((algebraMap ℚ A : (a : ℚ) → A)
            (bernoulli (n + 1 + 1) / (HAdd.hAdd (α := ℚ) (↑(n + 1) : ℚ) 1 * (↑(n + 1)! : ℚ))) :
          A)
        (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
      ((algebraMap ℚ A : (a : ℚ) → A)
          (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
            bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
        A) =
    if n + 1 + 1 = 1 then 1 else 0

Tactic:
rw [if_neg n.succ_succ_ne_one]

Premises used: Nat.succ_succ_ne_one, if_neg
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0

Tactic:
have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
⊢ Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0

Tactic:
have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
hite2 : Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0
h :
  Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
          bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
      A)
    (0 : A)
⊢ HAdd.hAdd (β := A)
      (HMul.hMul (α := A)
        ((algebraMap ℚ A : (a : ℚ) → A)
            (bernoulli (n + 1 + 1) / (HAdd.hAdd (α := ℚ) (↑(n + 1) : ℚ) 1 * (↑(n + 1)! : ℚ))) :
          A)
        (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
      ((algebraMap ℚ A : (a : ℚ) → A)
          (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
            bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
        A) =
    0

Tactic:
simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero]

Premises used: CharP.cast_eq_zero, inv_one, sub_self, zero_add, MulZeroClass.mul_zero, map_one
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
hite2 : Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0
h :
  Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
          bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
      A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ i ∈ @antidiagonal _ instAddMonoid _ n.succ,
          (↑((i.1 + i.2).choose i.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * bernoulli i.1 / (↑n.succ ! : ℚ)) :
      A)
⊢ Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
          bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
      A)
    (0 : A)

Tactic:
rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]

Premises used: Algebra.algebraMap, Rat, zero_div, bernoulli_spec', map_zero, Nat.cast, Finset.sum_div, Nat.factorial, Nat.succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
hite2 : Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0
⊢ Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
          bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
      A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ i ∈ @antidiagonal _ instAddMonoid _ n.succ,
          (↑((i.1 + i.2).choose i.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * bernoulli i.1 / (↑n.succ ! : ℚ)) :
      A)

Tactic:
congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)

Premises used: eq_div_of_mul_eq, Algebra.algebraMap, Rat, congr_arg, Nat.succ, DFunLike.coe, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
hite2 : Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0
h :
  ∀ (x : ℕ × ℕ) (h : x ∈ @antidiagonal _ instAddMonoid _ n.succ),
    bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n.succ ! : ℚ) =
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1
⊢ Eq (α := A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
          bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
      A)
    ((algebraMap ℚ A : (a : ℚ) → A)
        (∑ i ∈ @antidiagonal _ instAddMonoid _ n.succ,
          (↑((i.1 + i.2).choose i.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑i.2 : ℚ) 1 * bernoulli i.1 / (↑n.succ ! : ℚ)) :
      A)

Tactic:
refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)

Premises used: eq_div_of_mul_eq, Algebra.algebraMap, Rat, congr_arg, Nat.succ, DFunLike.coe, Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
hite2 : Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0
x : ℕ × ℕ
h : x ∈ @antidiagonal _ instAddMonoid _ n.succ
⊢ x.1 + x.2 = n.succ

Tactic:
rw [mem_antidiagonal] at h

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
hite2 : Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
h₁ :
  bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑(x.1 + x.2)! : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(x.1 + x.2)! : ℚ) (↑(x.1! * x.2!) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1
⊢ bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑n.succ ! : ℚ) =
    (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1

Tactic:
rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]

Premises used: Nat.factorial_mul_factorial_dvd_factorial_add, Nat.cast_div_charZero, Nat.add_choose
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
hite2 : Eq (α := ℚ) (if n.succ = 0 then 1 else 0) 0
x : ℕ × ℕ
h : x.1 + x.2 = n.succ
⊢ bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹ * (↑(x.1 + x.2)! : ℚ) =
    HDiv.hDiv (α := ℚ) (↑(x.1 + x.2)! : ℚ) (↑(x.1! * x.2!) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1

Tactic:
simp [field, mul_comm _ (bernoulli x.1), mul_assoc]

Premises used: bernoulli, mul_assoc, Prod.fst, mul_comm
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
h :
  HAdd.hAdd (β := A)
      (HMul.hMul (α := A)
        ((algebraMap ℚ A : (a : ℚ) → A)
            (bernoulli (HAdd.hAdd (α := ℕ) 0 1) / (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1 * (↑0! : ℚ))) :
          A)
        (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
      ((algebraMap ℚ A : (a : ℚ) → A)
          (∑ x ∈ @antidiagonal _ instAddMonoid _ 0,
            bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
        A) =
    if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0
h₁ :
  ∀ (n : ℕ),
    HAdd.hAdd (β := A)
        (HMul.hMul (α := A)
          ((algebraMap ℚ A : (a : ℚ) → A)
              (bernoulli (n + 1 + 1) / (HAdd.hAdd (α := ℚ) (↑(n + 1) : ℚ) 1 * (↑(n + 1)! : ℚ))) :
            A)
          (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
        ((algebraMap ℚ A : (a : ℚ) → A)
            (∑ x ∈ @antidiagonal _ instAddMonoid _ (n + 1),
              bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
          A) =
      if n + 1 + 1 = 1 then 1 else 0
⊢ HAdd.hAdd (β := A)
      (HMul.hMul (α := A)
        ((algebraMap ℚ A : (a : ℚ) → A) (bernoulli (n + 1) / (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 * (↑n ! : ℚ))) : A)
        (HSub.hSub (α := A) (β := A) ((algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1)⁻¹ : A) (1 : A)))
      ((algebraMap ℚ A : (a : ℚ) → A)
          (∑ x ∈ @antidiagonal _ instAddMonoid _ n,
            bernoulli x.1 / (↑x.1! : ℚ) * (HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * (↑x.2! : ℚ))⁻¹) :
        A) =
    if n + 1 = 1 then 1 else 0

Tactic:
cases n with | zero => simp | succ n =>
  rw [if_neg n.succ_succ_ne_one]
  have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
  have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero
  simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero]
  rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]
  refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)
  rw [mem_antidiagonal] at h
  rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]
  simp [field, mul_comm _ (bernoulli x.1), mul_assoc]

Premises used: CharP.cast_eq_zero, Algebra.algebraMap, inv_one, Nat.factorial_mul_factorial_dvd_factorial_add, sub_self, Rat, Nat.cast_div_charZero, mul_assoc, zero_div, bernoulli_spec', map_zero, zero_add, Nat.cast, Nat.succ_succ_ne_one, MulZeroClass.mul_zero, Finset.sum_div, Finset.HasAntidiagonal.mem_antidiagonal, Nat.factorial, map_one, Nat.zero, Nat.add_choose, Nat.succ, if_neg
-- 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) (bernoulliPowerSeries A * (exp A - 1)) : A) ((coeff 0 : (a : A⟦X⟧) → A) X : A)
h₁ :
  ∀ (n : ℕ),
    Eq (α := A) ((coeff (n + 1) : (a : A⟦X⟧) → A) (bernoulliPowerSeries A * (exp A - 1)) : A)
      ((coeff (n + 1) : (a : A⟦X⟧) → A) X : A)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulliPowerSeries A * (exp A - 1)) : A) ((coeff n : (a : A⟦X⟧) → A) X : A)

Tactic:
cases n with | zero => simp | succ n =>
  simp only [bernoulliPowerSeries, coeff_mul, coeff_X, sum_antidiagonal_succ', one_div, coeff_mk,
    coeff_one, coeff_exp, map_sub, factorial, if_pos, cast_succ, cast_mul,
    sub_zero, add_eq_zero, if_false, one_ne_zero, and_false, ← map_mul, ← map_sum]
  cases n with | zero => simp | succ n =>
  rw [if_neg n.succ_succ_ne_one]
  have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
  have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := if_neg n.succ_ne_zero
  simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero]
  rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]
  refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)
  rw [mem_antidiagonal] at h
  rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]
  simp [field, mul_comm _ (bernoulli x.1), mul_assoc]

Premises used: CharP.cast_eq_zero, Nat.cast_succ, map_sub, Algebra.algebraMap, inv_one, Nat.factorial_mul_factorial_dvd_factorial_add, sub_self, sub_zero, Rat, Nat.cast_div_charZero, mul_assoc, if_false, zero_div, bernoulli_spec', map_zero, PowerSeries.coeff_mk, PowerSeries.coeff_exp, if_pos, map_sum, zero_add, Nat.cast, Nat.succ_succ_ne_one, MulZeroClass.mul_zero, Finset.sum_div, PowerSeries.coeff_mul, map_mul, PowerSeries.coeff_X, Nat.cast_mul, Finset.HasAntidiagonal.mem_antidiagonal, Nat.factorial, map_one, PowerSeries.coeff_one, one_div, Nat.zero, Nat.add_choose, and_false, add_eq_zero, one_ne_zero, bernoulliPowerSeries, Nat.succ, if_neg, Finset.Nat.sum_antidiagonal_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
⊢ ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0

Tactic:
have hne : ∀ m : ℕ, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
h :
  ∀ (q : ℕ),
    Eq (α := ℚ)
      ((coeff q : (a : ℚ⟦X⟧) → ℚ)
          (HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
            (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))) :
        ℚ)
      ((coeff q : (a : ℚ⟦X⟧) → ℚ)
          (PowerSeries.mk fun (p : ℕ) ↦
            ∑ i ∈ range (p + 1),
              bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)) :
        ℚ)
⊢ HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
      (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n)) =
    PowerSeries.mk fun (p : ℕ) ↦
      ∑ i ∈ range (p + 1),
        bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)

Tactic:
ext q : 1
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
h :
  Eq (α := ℚ)
    (∑ x ∈ range q.succ,
      HMul.hMul (β := ℚ) (bernoulli x / (↑x ! : ℚ)) ((coeff (q - x + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ))
    (∑ i ∈ range (q + 1),
      bernoulli i * (↑((q + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - i) / (↑(q + 1)! : ℚ))
⊢ Eq (α := ℚ)
    ((coeff q : (a : ℚ⟦X⟧) → ℚ)
        (HMul.hMul (α := ℚ⟦X⟧) (PowerSeries.mk fun (p : ℕ) ↦ bernoulli p / (↑p ! : ℚ))
          (PowerSeries.mk fun (q : ℕ) ↦ (coeff (q + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n))) :
      ℚ)
    ((coeff q : (a : ℚ⟦X⟧) → ℚ)
        (PowerSeries.mk fun (p : ℕ) ↦
          ∑ i ∈ range (p + 1),
            bernoulli i * (↑((p + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (p + 1 - i) / (↑(p + 1)! : ℚ)) :
      ℚ)

Tactic:
simp only [f, coeff_mul, coeff_mk, sum_antidiagonal_eq_sum_range_succ f]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, PowerSeries.coeff_mk, PowerSeries.coeff_mul
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
h :
  ∀ x ∈ range q.succ,
    HMul.hMul (β := ℚ) (bernoulli x / (↑x ! : ℚ)) ((coeff (q - x + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ) =
      bernoulli x * (↑((q + 1).choose x) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - x) / (↑(q + 1)! : ℚ)
⊢ Eq (α := ℚ)
    (∑ x ∈ range q.succ,
      HMul.hMul (β := ℚ) (bernoulli x / (↑x ! : ℚ)) ((coeff (q - x + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ))
    (∑ i ∈ range (q + 1),
      bernoulli i * (↑((q + 1).choose i) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - i) / (↑(q + 1)! : ℚ))

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h : m ∈ range q.succ
h₁ :
  HMul.hMul (β := ℚ) (bernoulli m / (↑m ! : ℚ))
      ((coeff (q - m + 1) : (a : ℚ⟦X⟧) → ℚ)
          (({
                  toFun := fun (f : ℚ⟦X⟧) ↦
                    PowerSeries.mk fun (n_1 : ℕ) ↦
                      HMul.hMul (β := ℚ) (HPow.hPow (α := ℚ) (↑n : ℚ) n_1) ((coeff n_1 : (a : ℚ⟦X⟧) → ℚ) f : ℚ),
                  map_one' := ⋯, map_mul' := ⋯ : ℚ⟦X⟧ →* ℚ⟦X⟧ } :
                (a : ℚ⟦X⟧) → ℚ⟦X⟧)
              (exp ℚ) :
            ℚ⟦X⟧) :
        ℚ) =
    bernoulli m * (↑((q + 1).choose m) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) / (↑(q + 1)! : ℚ)
⊢ HMul.hMul (β := ℚ) (bernoulli m / (↑m ! : ℚ)) ((coeff (q - m + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ) =
    bernoulli m * (↑((q + 1).choose m) : ℚ) * HPow.hPow (α := ℚ) (↑n : ℚ) (q + 1 - m) / (↑(q + 1)! : ℚ)

Tactic:
simp only [exp_pow_eq_rescale_exp, rescale, RingHom.coe_mk]

Premises used: RingHom.coe_mk, PowerSeries.exp_pow_eq_rescale_exp, PowerSeries.rescale
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h : m ∈ range q.succ
⊢ m < q + 1

Tactic:
simpa using h
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n p : ℕ
hne : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
q : ℕ
f : (a b : ℕ) → ℚ :=
  fun (a b : ℕ) ↦ HMul.hMul (β := ℚ) (bernoulli a / (↑a ! : ℚ)) ((coeff (b + 1) : (a : ℚ⟦X⟧) → ℚ) (exp ℚ ^ n) : ℚ)
m : ℕ
h : m ∈ range q.succ
⊢ m < q + 1

Tactic:
have h : m < q + 1 := by simpa using h