n : ℕ
⊢ ∑ k in range (n + 1 - 0),
      ∑ k_1 in range (n + 1 - (0 + k)),
        ↑(Nat.choose (n + 1) (0 + k + k_1)) •
          ↑(monomial (0 + k)) (_root_.bernoulli (0 + k + k_1 - (0 + k)) * ↑(Nat.choose (0 + k + k_1) (0 + k))) =
    ↑(monomial n) (↑n + 1)
n : ℕ
⊢ ∑ k in range (n + 1), ↑(Nat.choose (n + 1) k) • bernoulli k = ↑(monomial n) (↑n + 1)
simp_rw [bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico, ← Finset.sum_Ico_Ico_comm,
  Finset.sum_Ico_eq_sum_range]
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        ↑(Nat.choose (n + 1) (x + x_1)) • ↑(monomial x) (_root_.bernoulli x_1 * ↑(Nat.choose (x + x_1) x)) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
n : ℕ
⊢ ∑ k in range (n + 1 - 0),
      ∑ k_1 in range (n + 1 - (0 + k)),
        ↑(Nat.choose (n + 1) (0 + k + k_1)) •
          ↑(monomial (0 + k)) (_root_.bernoulli (0 + k + k_1 - (0 + k)) * ↑(Nat.choose (0 + k + k_1) (0 + k))) =
    ↑(monomial n) (↑n + 1)
simp only [add_tsub_cancel_left, tsub_zero, zero_add, map_add]
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        ↑(monomial x) (↑(Nat.choose (n + 1) (x + x_1)) * ↑(Nat.choose (x + x_1) x) * _root_.bernoulli x_1) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        ↑(Nat.choose (n + 1) (x + x_1)) • ↑(monomial x) (_root_.bernoulli x_1 * ↑(Nat.choose (x + x_1) x)) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        (↑(Nat.choose (n + 1 - x) x_1) * _root_.bernoulli x_1) • ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        ↑(monomial x) (↑(Nat.choose (n + 1) (x + x_1)) * ↑(Nat.choose (x + x_1) x) * _root_.bernoulli x_1) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
conv_lhs =>
  apply_congr
  . skip
  . conv =>
    apply_congr
    . skip
    . rw [← Nat.cast_mul, choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <|
          mem_range_le (by assumption)) (le.intro rfl),
        Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ←
        smul_monomial]
n : ℕ
⊢ ∑ x in range (n + 1),
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
        ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
n : ℕ
⊢ ∑ x in range (n + 1),
      ∑ x_1 in range (n + 1 - x),
        (↑(Nat.choose (n + 1 - x) x_1) * _root_.bernoulli x_1) • ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
simp_rw [← sum_smul]
n : ℕ
⊢ (∑ i in range (n + 1 - n), ↑(Nat.choose (n + 1 - n) i) * _root_.bernoulli i) • ↑(monomial n) ↑(Nat.choose (n + 1) n) +
      ∑ x in range n,
        (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
n : ℕ
⊢ ∑ x in range (n + 1),
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
        ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
rw [sum_range_succ_comm]
n : ℕ
⊢ ∑ x in range n,
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
        ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    0
n : ℕ
⊢ (∑ i in range (n + 1 - n), ↑(Nat.choose (n + 1 - n) i) * _root_.bernoulli i) • ↑(monomial n) ↑(Nat.choose (n + 1) n) +
      ∑ x in range n,
        (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    ↑(monomial n) ↑n + ↑(monomial n) 1
simp only [add_right_eq_self, mul_one, cast_one, cast_add, add_tsub_cancel_left,
  choose_succ_self_right, one_smul, _root_.bernoulli_zero, sum_singleton, zero_add,
  map_add, range_one, bernoulli_zero, mul_one, one_mul, add_zero, choose_self]
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range n →
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
        0
n : ℕ
⊢ ∑ x in range n,
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
        ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    0
apply sum_eq_zero fun x hx => _
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
⊢ ∀ (x : ℕ),
    x ∈ range n →
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
        0
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range n →
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
        0
have f : ∀ x ∈ range n, ¬n + 1 - x = 1 := by
  rintro x H
  rw [mem_range] at H
  rw [eq_comm]
  exact _root_.ne_of_lt (Nat.lt_of_lt_of_le one_lt_two (le_tsub_of_add_le_left (succ_le_succ H)))
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) • ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    0
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
⊢ ∀ (x : ℕ),
    x ∈ range n →
      (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) •
          ↑(monomial x) ↑(Nat.choose (n + 1) x) =
        0
intro x hx
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (if n + 1 - x = 1 then 1 else 0) • ↑(monomial x) ↑(Nat.choose (n + 1) x) = 0
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (∑ i in range (n + 1 - x), ↑(Nat.choose (n + 1 - x) i) * _root_.bernoulli i) • ↑(monomial x) ↑(Nat.choose (n + 1) x) =
    0
rw [sum_bernoulli]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
g : (if n + 1 - x = 1 then 1 else 0) = 0
⊢ (if n + 1 - x = 1 then 1 else 0) • ↑(monomial x) ↑(Nat.choose (n + 1) x) = 0
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (if n + 1 - x = 1 then 1 else 0) • ↑(monomial x) ↑(Nat.choose (n + 1) x) = 0
have g : ite (n + 1 - x = 1) (1 : ℚ) 0 = 0 := by
  simp only [ite_eq_right_iff, one_ne_zero]
  intro h₁
  exact (f x hx) h₁
no goals
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
g : (if n + 1 - x = 1 then 1 else 0) = 0
⊢ (if n + 1 - x = 1 then 1 else 0) • ↑(monomial x) ↑(Nat.choose (n + 1) x) = 0
rw [g, zero_smul]
no goals
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ x✝¹ ∈ range (n + 1)
assumption
no goals
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ x✝ ∈ range (n + 1 - x✝¹)
assumption
n x : ℕ
H : x ∈ range n
⊢ ¬n + 1 - x = 1
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
rintro x H
n x : ℕ
H : x < n
⊢ ¬n + 1 - x = 1
n x : ℕ
H : x ∈ range n
⊢ ¬n + 1 - x = 1
rw [mem_range] at H
n x : ℕ
H : x < n
⊢ ¬1 = n + 1 - x
n x : ℕ
H : x < n
⊢ ¬n + 1 - x = 1
rw [eq_comm]
no goals
n x : ℕ
H : x < n
⊢ ¬1 = n + 1 - x
exact _root_.ne_of_lt (Nat.lt_of_lt_of_le one_lt_two (le_tsub_of_add_le_left (succ_le_succ H)))
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ n + 1 - x = 1 → False
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ (if n + 1 - x = 1 then 1 else 0) = 0
simp only [ite_eq_right_iff, one_ne_zero]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
h₁ : n + 1 - x = 1
⊢ False
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ n + 1 - x = 1 → False
intro h₁
no goals
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
h₁ : n + 1 - x = 1
⊢ False
exact (f x hx) h₁