awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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 :
  Eq (α := ℚ)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1)
⊢ ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1 =
    0 - (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli (1, n).1
have h₂ : 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: convert! eq_sub_of_add_eq' H using 1
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ Eq (α := ℚ)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1)
    (∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1)
have h : ∀ (p : ℕ × ℕ) (h : p ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(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: refine sum_congr rfl fun p h => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)}
⊢ p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ≠ (1, n)
have rwa : ∀ (h : p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ∉ {(1, n)}),
  p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ≠ (1, n)
Tactic: rwa [mem_sdiff, mem_singleton] at h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)}
rwa :
  ∀ (h : p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ∉ {(1, n)}),
    p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ≠ (1, n)
⊢ p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ≠ (1, n)
have rwa₁ : ∀ (h : p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ ¬p = (1, n)),
  p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ≠ (1, n)
Tactic: rwa [mem_sdiff, mem_singleton] at h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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)}
⊢ (↑((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
have h' : p ∈ @antidiagonal _ instAddMonoid _ n.succ
Tactic: obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ (↑((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
have h'' : p ≠ (1, n)
Tactic: obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ 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
have h : 1 = HSub.hSub (α := ℚ) 2 1
Tactic: simp [field, h₃]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
n : ℕ
⊢ 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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ bernoulliPowerSeries A * (exp A - 1) = X
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulliPowerSeries A * (exp A - 1)) : A) ((coeff n : (a : A⟦X⟧) → A) X : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
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)
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
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
have 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
Tactic: rw [if_neg n.succ_succ_ne_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
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) =
    0
have hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 0
Tactic: have hfact : ∀ m, (m ! : ℚ) ≠ 0 := fun m => mod_cast factorial_ne_zero m
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), Ne (α := ℚ) (↑m ! : ℚ) 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) =
    0
have hite2 : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ 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
have 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)
Tactic: simp only [CharP.cast_eq_zero, zero_add, inv_one, map_one, sub_self, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
    (0 : A)
have 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)
Tactic: rw [← map_zero (algebraMap ℚ A), ← zero_div (n.succ ! : ℚ), ← hite2, ← bernoulli_spec', sum_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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)
have 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
Tactic: refine congr_arg (algebraMap ℚ A) (sum_congr rfl fun x h => eq_div_of_mul_eq (hfact n.succ) ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (hypothesis)
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
⊢ 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
have h₁ : x.1 + x.2 = n.succ
Tactic: rw [mem_antidiagonal] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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! : ℚ))⁻¹ * (↑n.succ ! : ℚ) =
    (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli x.1
have 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
Tactic: rw [← h, add_choose, cast_div_charZero (factorial_mul_factorial_dvd_factorial_add _ _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ 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
have 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
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
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
⊢ 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
have 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
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]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Bernoulli (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) (bernoulliPowerSeries A * (exp A - 1)) : A) ((coeff n : (a : A⟦X⟧) → A) X : A)
have h : Eq (α := A) ((coeff 0 : (a : A⟦X⟧) → A) (bernoulliPowerSeries A * (exp A - 1)) : A) ((coeff 0 : (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]
Cleared hypotheses: n