case zero
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ∑ k in antidiagonal zero, ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst =
    if zero = 0 then 1 else 0

case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst =
    if succ n = 0 then 1 else 0
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in antidiagonal n, ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = if n = 0 then 1 else 0
cases' n with n n
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst =
    if succ n = 0 then 1 else 0
rw [if_neg (succ_ne_zero _)]
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
have h₁ : (1, n) ∈ antidiagonal n.succ := by simp [mem_antidiagonal, add_comm]
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
have h₂ : (n : ℚ) + 1 ≠ 0 := by norm_cast; exact succ_ne_zero _
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
have h₃ : (1 + n).choose n = n + 1 := by simp [add_comm]
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H : ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli' k.fst = 1
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
have H := bernoulli'_spec' n.succ
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst =
    0
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H : ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli' k.fst = 1
⊢ ∑ k in antidiagonal (succ n), ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst = 0
rw [sum_eq_add_sum_diff_singleton h₁] at H⊢
case succ.h
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst =
    0 - ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli (1, n).fst
case succ
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst =
    0
apply add_eq_of_eq_sub'
case h.e'_2
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst =
    ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst

case h.e'_3
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ 0 - ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli (1, n).fst =
    1 - ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst
case succ.h
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst =
    0 - ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli (1, n).fst
convert eq_sub_of_add_eq' H using 1
no goals
case zero
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ ∑ k in antidiagonal zero, ↑(Nat.choose (k.fst + k.snd) k.snd) / (↑k.snd + 1) * bernoulli k.fst =
    if zero = 0 then 1 else 0
simp
no goals
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ (1, n) ∈ antidiagonal (succ n)
simp [mem_antidiagonal, add_comm]
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
⊢ ¬n + 1 = 0
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
⊢ ↑n + 1 ≠ 0
norm_cast
no goals
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
⊢ ¬n + 1 = 0
exact succ_ne_zero _
no goals
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
⊢ Nat.choose (1 + n) n = n + 1
simp [add_comm]
case h.e'_2
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal (succ n) \ {(1, n)}
⊢ ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli p.fst =
    ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli' p.fst
case h.e'_2
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli x.fst =
    ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst
refine' sum_congr rfl fun p h => _
case h.e'_2.intro
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal (succ n) \ {(1, n)}
h' : p ∈ ?m.656139
h'' : p ≠ ?m.656186
⊢ ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli p.fst =
    ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli' p.fst
case h.e'_2
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal (succ n) \ {(1, n)}
⊢ ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli p.fst =
    ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli' p.fst
obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h
no goals
case h.e'_2.intro
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal (succ n) \ {(1, n)}
h' : p ∈ ?m.656139
h'' : p ≠ ?m.656186
⊢ ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli p.fst =
    ↑(Nat.choose (p.fst + p.snd) p.snd) / (↑p.snd + 1) * bernoulli' p.fst
simp [bernoulli_eq_bernoulli'_of_ne_one ((not_congr (antidiagonal_congr h' h₁)).mp h'')]
no goals
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal (succ n) \ {(1, n)}
⊢ p ∈ ?m.656139 ∧ p ≠ ?m.656186
rwa [mem_sdiff, mem_singleton] at h
case h.e'_3
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ 1 = 2 - 1
case h.e'_3
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ 0 - ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli (1, n).fst =
    1 - ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst
field_simp [h₃]
no goals
case h.e'_3
A : Type ?u.640965
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
h₁ : (1, n) ∈ antidiagonal (succ n)
h₂ : ↑n + 1 ≠ 0
h₃ : Nat.choose (1 + n) n = n + 1
H :
  ↑(Nat.choose ((1, n).fst + (1, n).snd) (1, n).snd) / (↑(1, n).snd + 1) * bernoulli' (1, n).fst +
      ∑ x in antidiagonal (succ n) \ {(1, n)}, ↑(Nat.choose (x.fst + x.snd) x.snd) / (↑x.snd + 1) * bernoulli' x.fst =
    1
⊢ 1 = 2 - 1
norm_num