awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℚ
suffices :
  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:
suffices evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ by
    simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_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 ℚ
⊢ HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) (B * (exp ℚ - 1)) : ℚ⟦X⟧) (exp ℚ) =
    HMul.hMul (α := ℚ⟦X⟧) ((evalNegHom : (a : ℚ⟦X⟧) → ℚ⟦X⟧) (X * exp ℚ) : ℚ⟦X⟧) (exp ℚ)

Tactic:
congr
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
⊢ bernoulli' n = HPow.hPow (α := ℚ) (-1) n * bernoulli n

Tactic:
simp [bernoulli, ← mul_assoc, ← sq, ← pow_mul, mul_comm n 2]

Premises used: bernoulli, mul_assoc, sq, pow_mul, mul_comm, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ bernoulli 0 = 1

Tactic:
simp [bernoulli]

Premises used: bernoulli
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ bernoulli 1 = -1 / 2

Tactic:
norm_num [bernoulli]

Premises used: bernoulli
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ bernoulli 2 = 6⁻¹

Tactic:
simp [bernoulli]

Premises used: bernoulli
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h_odd : Odd n
hlt : 1 < n
rw : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = 0
rw₁ : HPow.hPow (α := ℚ) (-1) n * 0 = 0
rw₂ rw₃ : Eq (α := ℚ) 0 0
⊢ bernoulli n = 0

Tactic:
rw [bernoulli, bernoulli'_eq_zero_of_odd h_odd hlt, mul_zero]

Premises used: bernoulli, MulZeroClass.mul_zero, bernoulli'_eq_zero_of_odd
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
hn : n ≠ 1
hlt : n < 1
⊢ bernoulli n = bernoulli' n

Tactic:
simp [lt_one_iff.mp hlt]

Premises used: Nat.lt_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
heven : Even n
inr : HPow.hPow (α := ℚ) (-1) n * bernoulli' n = bernoulli' n
inr₁ : 1 * bernoulli' n = bernoulli' n
inr₂ inr₃ : bernoulli' n = bernoulli' n
⊢ bernoulli n = bernoulli' n

Tactic:
rw [bernoulli, heven.neg_one_pow, one_mul]

Premises used: bernoulli, Even.neg_one_pow, one_mul
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
hodd : Odd n
inr : bernoulli n = 0
inr₁ inr₂ : Eq (α := ℚ) 0 0
⊢ bernoulli n = bernoulli' n

Tactic:
rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]

Premises used: bernoulli_eq_zero_of_odd, bernoulli'_eq_zero_of_odd
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
hn : n ≠ 1
hgt : 1 < n
⊢ Even n ∨ Odd n

Tactic:
cases n.even_or_odd with
    | inl heven => rw [bernoulli, heven.neg_one_pow, one_mul]
    | inr hodd => rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]

Premises used: bernoulli, Nat.even_or_odd, one_mul
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
hn : n ≠ 1
⊢ n < 1 ∨ 1 < n

Tactic:
cases hn.lt_or_gt with
  | inl hlt => simp [lt_one_iff.mp hlt]
  | inr hgt =>
    cases n.even_or_odd with
    | inl heven => rw [bernoulli, heven.neg_one_pow, one_mul]
    | inr hodd => rw [bernoulli'_eq_zero_of_odd hodd hgt, bernoulli_eq_zero_of_odd hodd hgt]

Premises used: bernoulli, Nat.even_or_odd, one_mul, Ne.lt_or_gt
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ Eq (α := ℚ) (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) * bernoulli k) (if Eq (α := ℕ) 0 1 then 1 else 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ Eq (α := ℚ) (∑ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), (↑((HAdd.hAdd (α := ℕ) 0 1).choose k) : ℚ) * bernoulli k)
    (if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
this : ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
simp : HDiv.hDiv (α := ℚ) (↑n : ℚ) 2 + (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1) * (-1 / 2) + 1 = 0
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1 + 1), (↑((n + 1 + 1).choose k) : ℚ) * bernoulli k) (if n + 1 + 1 = 1 then 1 else 0)

Tactic:
simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]

Premises used: Nat.cast_succ, if_false, bernoulli_zero, zero_add, Nat.choose_one_right, Nat.succ_succ_ne_one, Nat.cast_zero, mul_one, bernoulli_one, Finset.sum_range_succ', Nat.choose_zero_right
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
this : ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
⊢ HDiv.hDiv (α := ℚ) (↑n : ℚ) 2 + (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1) * (-1 / 2) + 1 = 0

Tactic:
ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
succ : ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1 + 1), (↑((n + 1 + 1).choose k) : ℚ) * bernoulli k) (if n + 1 + 1 = 1 then 1 else 0)

Tactic:
suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
⊢ Eq (α := ℚ) (∑ k ∈ range n.succ.succ, (↑(n.succ.succ.choose k) : ℚ) * bernoulli' k) (↑n.succ.succ : ℚ)

Tactic:
have f := sum_bernoulli' n.succ.succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f : Eq (α := ℚ) (∑ k ∈ range n.succ.succ, (↑(n.succ.succ.choose k) : ℚ) * bernoulli' k) (↑n.succ.succ : ℚ)
⊢ ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f

Premises used: Nat.cast_succ, eq_sub_iff_add_eq, Finset.sum_range_succ'
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
⊢ ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2

Tactic:
Eq.trans ?_ (Eq.trans f ?_)

Premises used: Eq.trans
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
succ :
  Eq (α := ℚ) (∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2))
    (∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1))
succ₁ :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1) =
    HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
⊢ ∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2) = HDiv.hDiv (α := ℚ) (↑n : ℚ) 2

Tactic:
refine Eq.trans ?_ (Eq.trans f ?_)

Premises used: Eq.trans
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
succ :
  Eq (α := ℕ → ℚ) (fun (i : ℕ) ↦ (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2)) fun (k : ℕ) ↦
    (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1)
⊢ Eq (α := ℚ) (∑ i ∈ range n, (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2))
    (∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1))

Tactic:
congr
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
succ :
  ∀ (x : ℕ),
    (↑((n + 2).choose (x + 2)) : ℚ) * bernoulli (x + 2) =
      (↑(n.succ.succ.choose (x + 1 + 1)) : ℚ) * bernoulli' (x + 1 + 1)
⊢ Eq (α := ℕ → ℚ) (fun (i : ℕ) ↦ (↑((n + 2).choose (i + 2)) : ℚ) * bernoulli (i + 2)) fun (k : ℕ) ↦
    (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1)

Tactic:
funext x
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
x : ℕ
succ succ₁ :
  (↑((n + 2).choose (x + 2)) : ℚ) * bernoulli' x.succ.succ =
    (↑(n.succ.succ.choose (x + 1 + 1)) : ℚ) * bernoulli' (x + 1 + 1)
⊢ (↑((n + 2).choose (x + 2)) : ℚ) * bernoulli (x + 2) = (↑(n.succ.succ.choose (x + 1 + 1)) : ℚ) * bernoulli' (x + 1 + 1)

Tactic:
rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]

Premises used: Function.comp, Nat.succ.inj, Nat.succ_ne_zero, bernoulli_eq_bernoulli'_of_ne_one
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
succ :
  HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1 - (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1) * (1 / 2) =
    HDiv.hDiv (α := ℚ) (↑n : ℚ) 2
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1) =
    HDiv.hDiv (α := ℚ) (↑n : ℚ) 2

Tactic:
simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]

Premises used: Nat.cast_succ, zero_add, Nat.choose_one_right, bernoulli'_one, mul_one, Nat.choose_zero_right, bernoulli'_zero
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
f :
  ∑ k ∈ range n, (↑(n.succ.succ.choose (k + 1 + 1)) : ℚ) * bernoulli' (k + 1 + 1) =
    HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - (↑(n.succ.succ.choose 0) : ℚ) * bernoulli' 0 -
      (↑(n.succ.succ.choose (HAdd.hAdd (α := ℕ) 0 1)) : ℚ) * bernoulli' (HAdd.hAdd (α := ℕ) 0 1)
⊢ HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1 - HAdd.hAdd (α := ℚ) (↑0 : ℚ) 1 - (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1 + 1) * (1 / 2) =
    HDiv.hDiv (α := ℚ) (↑n : ℚ) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
succ :
  Eq (α := ℚ) (∑ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), (↑((HAdd.hAdd (α := ℕ) 0 1).choose k) : ℚ) * bernoulli k)
    (if HAdd.hAdd (α := ℕ) 0 1 = 1 then 1 else 0)
succ₁ :
  ∀ (n : ℕ),
    Eq (α := ℚ) (∑ k ∈ range (n + 1 + 1), (↑((n + 1 + 1).choose k) : ℚ) * bernoulli k) (if n + 1 + 1 = 1 then 1 else 0)
⊢ Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli k) (if n + 1 = 1 then 1 else 0)

Tactic:
cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring

Premises used: Nat.cast_succ, eq_sub_iff_add_eq, zero_add, Nat.choose_one_right, bernoulli'_one, Nat.zero, mul_one, Nat.succ, Finset.sum_range_succ', Nat.choose_zero_right, bernoulli'_zero
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
zero : Eq (α := ℚ) (∑ k ∈ range 0, (↑(Nat.choose 0 k) : ℚ) * bernoulli k) (if Eq (α := ℕ) 0 1 then 1 else 0)
succ :
  ∀ (n : ℕ), Eq (α := ℚ) (∑ k ∈ range (n + 1), (↑((n + 1).choose k) : ℚ) * bernoulli k) (if n + 1 = 1 then 1 else 0)
⊢ Eq (α := ℚ) (∑ k ∈ range n, (↑(n.choose k) : ℚ) * bernoulli k) (if n = 1 then 1 else 0)

Tactic:
cases n with | zero => simp | succ n =>
  cases n with
  | zero => simp
  | succ n =>
  suffices (∑ i ∈ range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2)) = n / 2 by
    simp only [this, sum_range_succ', cast_succ, bernoulli_one, bernoulli_zero, choose_one_right,
      mul_one, choose_zero_right, cast_zero, if_false, zero_add, succ_succ_ne_one]
    ring
  have f := sum_bernoulli' n.succ.succ
  simp_rw [sum_range_succ', cast_succ, ← eq_sub_iff_add_eq] at f
  refine Eq.trans ?_ (Eq.trans f ?_)
  · congr
    funext x
    rw [bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj)]
  · simp only [mul_one, bernoulli'_zero, choose_zero_right,
      zero_add, choose_one_right, cast_succ, bernoulli'_one]
    ring

Premises used: Nat.cast_succ, eq_sub_iff_add_eq, zero_add, Nat.choose_one_right, bernoulli'_one, Nat.zero, mul_one, Nat.succ, Finset.sum_range_succ', Nat.choose_zero_right, bernoulli'_zero
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
⊢ 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:
simp
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
⊢ (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ

Tactic:
simp [mem_antidiagonal, add_comm]

Premises used: add_comm, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
⊢ (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ

Tactic:
have h₁ : (1, n) ∈ antidiagonal n.succ := by simp [mem_antidiagonal, add_comm]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
⊢ (1 + n).choose n = n + 1

Tactic:
simp [add_comm]

Premises used: add_comm
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
⊢ (1 + n).choose n = n + 1

Tactic:
have h₃ : (1 + n).choose n = n + 1 := by simp [add_comm]
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n.succ,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
    1

Tactic:
have H := bernoulli'_spec' n.succ
-- Module: Mathlib.NumberTheory.Bernoulli
Goal:
n : ℕ
h₁ : (1, n) ∈ @antidiagonal _ instAddMonoid _ n.succ
h₃ : (1 + n).choose n = n + 1
H :
  Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ n.succ,
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli' k.1)
    1
succ :
  ∀
    (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, 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 =
      0
⊢ Eq (α := ℚ)
    (∑ k ∈ @antidiagonal _ instAddMonoid _ (n + 1),
      (↑((k.1 + k.2).choose k.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑k.2 : ℚ) 1 * bernoulli k.1)
    0

Tactic:
rw [sum_eq_add_sum_diff_singleton_of_mem h₁] at H ⊢

Premises used: Finset.sum_eq_add_sum_diff_singleton_of_mem
-- 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
succ :
  ∑ 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
⊢ (↑(((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 =
    0

Tactic:
apply add_eq_of_eq_sub'

Premises used: add_eq_of_eq_sub'
-- 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
⊢ ∑ x ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)},
      (↑((x.1 + x.2).choose x.2) : ℚ) / HAdd.hAdd (α := ℚ) (↑x.2 : ℚ) 1 * bernoulli' x.1 =
    1 - (↑(((1, n).1 + (1, n).2).choose (1, n).2) : ℚ) / HAdd.hAdd (α := ℚ) (↑(1, n).2 : ℚ) 1 * bernoulli' (1, n).1

Tactic:
eq_sub_of_add_eq' H

Premises used: eq_sub_of_add_eq'
-- 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 :
  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)
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
⊢ ∑ 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

Tactic:
convert! eq_sub_of_add_eq' H using 1

Premises used: eq_sub_of_add_eq'
-- 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
⊢ 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)

Tactic:
sum_congr rfl fun p h => ?_

Premises used: Finset.sum_congr, rfl
-- 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 :
  ∀ (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
⊢ 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)

Tactic:
refine sum_congr rfl fun p h => ?_

Premises used: Finset.sum_congr, rfl
-- 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)}
rwa :
  ∀ (h : p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ∉ {(1, n)}),
    p ∈ @antidiagonal _ instAddMonoid _ n.succ ∧ p ≠ (1, n)
rwa₁ rwa₂ rwa₃ 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)

Tactic:
rwa [mem_sdiff, mem_singleton] at h

Premises used: Finset.mem_singleton, Finset.mem_sdiff
-- 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)}
⊢ p ∈ @antidiagonal _ instAddMonoid _ n.succ

Tactic:
obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at 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
p : ℕ × ℕ
h : p ∈ @antidiagonal _ instAddMonoid _ n.succ \ {(1, n)}
h' : p ∈ @antidiagonal _ instAddMonoid _ n.succ
⊢ p ≠ (1, n)

Tactic:
obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h