[GOAL]
n : ℕ
⊢ bernoulli n = ∑ i in range (n + 1), ↑(monomial i) (_root_.bernoulli (n - i) * ↑(Nat.choose n i))
[PROOFSTEP]
rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]
[GOAL]
n : ℕ
⊢ ∑ i in range (n + 1), ↑(monomial (n - i)) (_root_.bernoulli i * ↑(Nat.choose n i)) =
    ∑ j in range (n + 1), ↑(monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(Nat.choose n (n - j)))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) →
      ↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x)) =
        ↑(monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(Nat.choose n (n - x)))
[PROOFSTEP]
rintro x hx
[GOAL]
n x : ℕ
hx : x ∈ range (n + 1)
⊢ ↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x)) =
    ↑(monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(Nat.choose n (n - x)))
[PROOFSTEP]
rw [mem_range_succ_iff] at hx 
[GOAL]
n x : ℕ
hx : x ≤ n
⊢ ↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x)) =
    ↑(monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(Nat.choose n (n - x)))
[PROOFSTEP]
rw [choose_symm hx, tsub_tsub_cancel_of_le hx]
[GOAL]
⊢ bernoulli 0 = 1
[PROOFSTEP]
simp [bernoulli]
[GOAL]
n : ℕ
⊢ eval 0 (bernoulli n) = _root_.bernoulli n
[PROOFSTEP]
rw [bernoulli, eval_finset_sum, sum_range_succ]
[GOAL]
n : ℕ
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
[PROOFSTEP]
have : (∑ x : ℕ in range n, _root_.bernoulli x * n.choose x * 0 ^ (n - x)) = 0 :=
  by
  apply sum_eq_zero <| fun x hx => _
  intros x hx
  have h : x < n := (mem_range.1 hx)
  simp [h]
[GOAL]
n : ℕ
⊢ ∑ x in range n, _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
apply sum_eq_zero <| fun x hx => _
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
intros x hx
[GOAL]
n x : ℕ
hx : x ∈ range n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
have h : x < n := (mem_range.1 hx)
[GOAL]
n x : ℕ
hx : x ∈ range n
h : x < n
⊢ _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
[PROOFSTEP]
simp [h]
[GOAL]
n : ℕ
this : ∑ x in range n, _root_.bernoulli x * ↑(Nat.choose n x) * 0 ^ (n - x) = 0
⊢ ∑ x in range n, eval 0 (↑(monomial (n - x)) (_root_.bernoulli x * ↑(Nat.choose n x))) +
      eval 0 (↑(monomial (n - n)) (_root_.bernoulli n * ↑(Nat.choose n n))) =
    _root_.bernoulli n
[PROOFSTEP]
simp [this]
[GOAL]
n : ℕ
⊢ eval 1 (bernoulli n) = bernoulli' n
[PROOFSTEP]
simp only [bernoulli, eval_finset_sum]
[GOAL]
n : ℕ
⊢ ∑ i in range (n + 1), eval 1 (↑(monomial (n - i)) (_root_.bernoulli i * ↑(Nat.choose n i))) = bernoulli' n
[PROOFSTEP]
simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self, (_root_.bernoulli _).mul_comm,
  sum_bernoulli, one_pow, mul_one, eval_C, eval_monomial, one_mul]
[GOAL]
n : ℕ
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
by_cases h : n = 1
[GOAL]
case pos
n : ℕ
h : n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
simp [h]
[GOAL]
case pos
n : ℕ
h : n = 1
⊢ 1 + -1 / 2 = 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
case neg
n : ℕ
h : ¬n = 1
⊢ (if n = 1 then 1 else 0) + _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
simp [h]
[GOAL]
case neg
n : ℕ
h : ¬n = 1
⊢ _root_.bernoulli n = bernoulli' n
[PROOFSTEP]
exact bernoulli_eq_bernoulli'_of_ne_one h
[GOAL]
k : ℕ
⊢ ↑derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k
[PROOFSTEP]
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]
  -- LHS sum has an extra term, but the coefficient is zero:
[GOAL]
k : ℕ
⊢ ∑ x in range (k + 1 + 1), ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose (k + 1) x) * ↑(k + 1 - x)) =
    (↑k + 1) * ∑ x in range (k + 1), ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose k x))
[PROOFSTEP]
rw [range_add_one, sum_insert not_mem_range_self, tsub_self, cast_zero, mul_zero, map_zero, zero_add, mul_sum]
  -- the rest of the sum is termwise equal:
[GOAL]
k : ℕ
⊢ ∑ x in range (k + 1), ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose (k + 1) x) * ↑(k + 1 - x)) =
    ∑ x in range (k + 1), (↑k + 1) * ↑(monomial (k - x)) (_root_.bernoulli x * ↑(Nat.choose k x))
[PROOFSTEP]
refine' sum_congr (by rfl) fun m _ => _
[GOAL]
k : ℕ
⊢ range (k + 1) = range (k + 1)
[PROOFSTEP]
rfl
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose (k + 1) m) * ↑(k + 1 - m)) =
    (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
| (↑k + 1) * ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m))
[PROOFSTEP]
rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose (k + 1) m) * ↑(k + 1 - m)) =
    ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m) * ↑(k + 1))
[PROOFSTEP]
rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
[GOAL]
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose (k + 1) m * (k + 1 - m))) =
    ↑(monomial (k - m)) (_root_.bernoulli m * ↑(Nat.choose k m * (k + 1)))
[PROOFSTEP]
congr 3
[GOAL]
case h.e_6.h.e_a.e_a
k m : ℕ
x✝ : m ∈ range (k + 1)
⊢ Nat.choose (k + 1) m * (k + 1 - m) = Nat.choose k m * (k + 1)
[PROOFSTEP]
rw [(choose_mul_succ_eq k m).symm, mul_comm]
[GOAL]
k : ℕ
⊢ ↑derivative (bernoulli k) = ↑k * bernoulli (k - 1)
[PROOFSTEP]
cases k with
| zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
| succ k => exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
k : ℕ
⊢ ↑derivative (bernoulli k) = ↑k * bernoulli (k - 1)
[PROOFSTEP]
cases k with
| zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
| succ k => exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
case zero
⊢ ↑derivative (bernoulli Nat.zero) = ↑Nat.zero * bernoulli (Nat.zero - 1)
[PROOFSTEP]

| zero => rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
[GOAL]
case zero
⊢ ↑derivative (bernoulli Nat.zero) = ↑Nat.zero * bernoulli (Nat.zero - 1)
[PROOFSTEP]
rw [Nat.cast_zero, zero_mul, bernoulli_zero, derivative_one]
[GOAL]
case succ
k : ℕ
⊢ ↑derivative (bernoulli (succ k)) = ↑(succ k) * bernoulli (succ k - 1)
[PROOFSTEP]

| succ k => exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
case succ
k : ℕ
⊢ ↑derivative (bernoulli (succ k)) = ↑(succ k) * bernoulli (succ k - 1)
[PROOFSTEP]
exact_mod_cast derivative_bernoulli_add_one k
[GOAL]
n : ℕ
⊢ ∑ k in range (n + 1), ↑(Nat.choose (n + 1) k) • bernoulli k = ↑(monomial n) (↑n + 1)
[PROOFSTEP]
simp_rw [bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico, ← Finset.sum_Ico_Ico_comm, Finset.sum_Ico_eq_sum_range]
[GOAL]
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)
[PROOFSTEP]
simp only [add_tsub_cancel_left, tsub_zero, zero_add, map_add]
[GOAL]
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
[PROOFSTEP]
simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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)
[PROOFSTEP]
  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]
[GOAL]
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)
[PROOFSTEP]
  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]
[GOAL]
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)
[PROOFSTEP]
apply_congr
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
case a
n x✝ : ℕ
a✝ : x✝ ∈ ?s₂
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
·skip
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n : ℕ
⊢ range (n + 1) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
·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]
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
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]
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
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]
[GOAL]
case a
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ ∑ x in range (n + 1 - x✝),
      ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x) =
    ?g x✝
[PROOFSTEP]
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]
[GOAL]
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
| ∑ x in range (n + 1 - x✝),
    ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x)
[PROOFSTEP]
  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]
[GOAL]
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
| ∑ x in range (n + 1 - x✝),
    ↑(monomial x✝) (↑(Nat.choose (n + 1) (x✝ + x)) * ↑(Nat.choose (x✝ + x) x✝) * _root_.bernoulli x)
[PROOFSTEP]
apply_congr
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ ?s₂
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
·skip
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case h
n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ range (n + 1 - x✝) = ?s₂
[PROOFSTEP]
skip
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
·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]
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
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]
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
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]
[GOAL]
case a
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ ↑(monomial x✝¹) (↑(Nat.choose (n + 1) (x✝¹ + x✝)) * ↑(Nat.choose (x✝¹ + x✝) x✝¹) * _root_.bernoulli x✝) = ?g x✝
[PROOFSTEP]
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]
[GOAL]
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ x✝¹ ∈ range (n + 1)
[PROOFSTEP]
assumption
[GOAL]
n x✝¹ : ℕ
a✝¹ : x✝¹ ∈ range (n + 1)
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - x✝¹)
⊢ x✝ ∈ range (n + 1 - x✝¹)
[PROOFSTEP]
assumption
[GOAL]
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
[PROOFSTEP]
simp_rw [← sum_smul]
[GOAL]
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
[PROOFSTEP]
rw [sum_range_succ_comm]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
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
[PROOFSTEP]
apply sum_eq_zero fun x hx => _
[GOAL]
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
[PROOFSTEP]
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)))
[GOAL]
n : ℕ
⊢ ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
[PROOFSTEP]
rintro x H
[GOAL]
n x : ℕ
H : x ∈ range n
⊢ ¬n + 1 - x = 1
[PROOFSTEP]
rw [mem_range] at H 
[GOAL]
n x : ℕ
H : x < n
⊢ ¬n + 1 - x = 1
[PROOFSTEP]
rw [eq_comm]
[GOAL]
n x : ℕ
H : x < n
⊢ ¬1 = n + 1 - x
[PROOFSTEP]
exact _root_.ne_of_lt (Nat.lt_of_lt_of_le one_lt_two (le_tsub_of_add_le_left (succ_le_succ H)))
[GOAL]
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
[PROOFSTEP]
intro x hx
[GOAL]
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
[PROOFSTEP]
rw [sum_bernoulli]
[GOAL]
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
[PROOFSTEP]
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₁
[GOAL]
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
[PROOFSTEP]
simp only [ite_eq_right_iff, one_ne_zero]
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
⊢ n + 1 - x = 1 → False
[PROOFSTEP]
intro h₁
[GOAL]
n : ℕ
f : ∀ (x : ℕ), x ∈ range n → ¬n + 1 - x = 1
x : ℕ
hx : x ∈ range n
h₁ : n + 1 - x = 1
⊢ False
[PROOFSTEP]
exact (f x hx) h₁
[GOAL]
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
[PROOFSTEP]
rw [g, zero_smul]
[GOAL]
n : ℕ
⊢ ↑(succ n) • bernoulli n = ↑(monomial n) ↑(succ n) - ∑ k in range n, ↑(Nat.choose (n + 1) k) • bernoulli k
[PROOFSTEP]
rw [Nat.cast_succ, ← sum_bernoulli n, sum_range_succ, add_sub_cancel', choose_succ_self_right, Nat.cast_succ]
[GOAL]
n p : ℕ
⊢ (↑p + 1) * ∑ k in range n, ↑k ^ p = eval (↑n) (bernoulli (succ p)) - _root_.bernoulli (succ p)
[PROOFSTEP]
rw [sum_range_pow, bernoulli_def, eval_finset_sum, ← sum_div, mul_div_cancel' _ _]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ i in range (succ p + 1), eval (↑n) (↑(monomial i) (_root_.bernoulli (succ p - i) * ↑(Nat.choose (succ p) i))) -
      _root_.bernoulli (succ p)
[PROOFSTEP]
simp_rw [eval_monomial]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x) =
    ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p)
[PROOFSTEP]
symm
[GOAL]
n p : ℕ
⊢ ∑ x in range (succ p + 1), _root_.bernoulli (succ p - x) * ↑(Nat.choose (succ p) x) * ↑n ^ x -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
rw [← sum_flip _, sum_range_succ]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1),
          _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) +
        _root_.bernoulli (succ p - (p + 1 - (p + 1))) * ↑(Nat.choose (succ p) (p + 1 - (p + 1))) *
          ↑n ^ (p + 1 - (p + 1)) -
      _root_.bernoulli (succ p) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
simp only [tsub_self, tsub_zero, choose_zero_right, cast_one, mul_one, _root_.pow_zero, add_tsub_cancel_right]
[GOAL]
n p : ℕ
⊢ ∑ x in range (p + 1),
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    ∑ x in range (p + 1), _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
apply sum_congr rfl fun x hx => _
[GOAL]
n p : ℕ
⊢ ∀ (x : ℕ),
    x ∈ range (p + 1) →
      _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
        _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
intro x hx
[GOAL]
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) * ↑(Nat.choose (succ p) (p + 1 - x)) * ↑n ^ (p + 1 - x) =
    _root_.bernoulli x * ↑(Nat.choose (p + 1) x) * ↑n ^ (p + 1 - x)
[PROOFSTEP]
apply congr_arg₂ _ (congr_arg₂ _ _ _) rfl
[GOAL]
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ _root_.bernoulli (succ p - (p + 1 - x)) = _root_.bernoulli x
[PROOFSTEP]
rw [Nat.sub_sub_self (mem_range_le hx)]
[GOAL]
n p x : ℕ
hx : x ∈ range (p + 1)
⊢ ↑(Nat.choose (succ p) (p + 1 - x)) = ↑(Nat.choose (p + 1) x)
[PROOFSTEP]
rw [← choose_symm (mem_range_le hx)]
[GOAL]
n p : ℕ
⊢ ↑p + 1 ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n p : ℕ
⊢ ¬p + 1 = 0
[PROOFSTEP]
apply succ_ne_zero _
[GOAL]
n p : ℕ
⊢ eval (↑n) (bernoulli (succ p)) = _root_.bernoulli (succ p) + (↑p + 1) * ∑ k in range n, ↑k ^ p
[PROOFSTEP]
apply eq_add_of_sub_eq'
[GOAL]
case h
n p : ℕ
⊢ eval (↑n) (bernoulli (succ p)) - _root_.bernoulli (succ p) = (↑p + 1) * ∑ k in range n, ↑k ^ p
[PROOFSTEP]
rw [sum_range_pow_eq_bernoulli_sub]
[GOAL]
n : ℕ
x : ℚ
⊢ eval (1 + x) (bernoulli n) = eval x (bernoulli n) + ↑n * x ^ (n - 1)
[PROOFSTEP]
refine' Nat.strong_induction_on n fun d hd => _
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)
[PROOFSTEP]
have nz : ((d.succ : ℕ) : ℚ) ≠ 0 := by norm_cast
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
⊢ ↑(succ d) ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (bernoulli d) = eval x (bernoulli d) + ↑d * x ^ (d - 1)
[PROOFSTEP]
apply (mul_right_inj' nz).1
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ ↑(succ d) * eval (1 + x) (bernoulli d) = ↑(succ d) * (eval x (bernoulli d) + ↑d * x ^ (d - 1))
[PROOFSTEP]
rw [← smul_eq_mul, ← eval_smul, bernoulli_eq_sub_sum, mul_add, ← smul_eq_mul, ← eval_smul, bernoulli_eq_sub_sum,
  eval_sub, eval_finset_sum]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i) =
    eval x (↑(monomial d) ↑(succ d) - ∑ k in range d, ↑(Nat.choose (d + 1) k) • bernoulli k) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
conv_lhs =>
  congr
  ·skip
  · apply_congr
    ·skip
    ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  congr
  ·skip
  · apply_congr
    ·skip
    ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  congr
  ·skip
  · apply_congr
    ·skip
    ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
congr
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
·skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| eval (1 + x) (↑(monomial d) ↑(succ d))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
· apply_congr
  ·skip
  ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  apply_congr
  ·skip
  ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
  apply_congr
  ·skip
  ·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ i in range d, eval (1 + x) (↑(Nat.choose (d + 1) i) • bernoulli i)
[PROOFSTEP]
apply_congr
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ ?a.s₂
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
·skip
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
[PROOFSTEP]
skip
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
[PROOFSTEP]
skip
[GOAL]
case a.h
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ range d = ?a.s₂
[PROOFSTEP]
skip
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
·rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ eval (1 + x) (↑(Nat.choose (d + 1) x✝) • bernoulli x✝) = ?a.g x✝
[PROOFSTEP]
rw [eval_smul, hd _ (mem_range.1 (by assumption))]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range d
⊢ x✝ ∈ range d
[PROOFSTEP]
assumption
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) -
      ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (eval x (bernoulli x_1) + ↑x_1 * x ^ (x_1 - 1)) =
    eval x (↑(monomial d) ↑(succ d) - ∑ k in range d, ↑(Nat.choose (d + 1) k) • bernoulli k) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
rw [eval_sub, eval_finset_sum]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) -
      ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (eval x (bernoulli x_1) + ↑x_1 * x ^ (x_1 - 1)) =
    eval x (↑(monomial d) ↑(succ d)) - ∑ i in range d, eval x (↑(Nat.choose (d + 1) i) • bernoulli i) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
simp_rw [eval_smul, smul_add]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) -
      ∑ x_1 in range d,
        (↑(Nat.choose (d + 1) x_1) • eval x (bernoulli x_1) + ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))) =
    eval x (↑(monomial d) ↑(succ d)) - ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • eval x (bernoulli x_1) +
      ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
rw [sum_add_distrib, sub_add, sub_eq_sub_iff_sub_eq_sub, _root_.add_sub_sub_cancel]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) - eval x (↑(monomial d) ↑(succ d)) =
    ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
conv_rhs =>
  congr
  ·skip
  · congr
    rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  ·skip
  · congr
    rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  ·skip
  · congr
    rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
congr
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
·skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
skip
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
· congr
  rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
  congr
  rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
case a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
congr
[GOAL]
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑(succ d)
case a.a
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
| ↑d * x ^ (d - 1)
[PROOFSTEP]
rw [succ_eq_add_one, ← choose_succ_self_right d]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ eval (1 + x) (↑(monomial d) ↑(succ d)) - eval x (↑(monomial d) ↑(succ d)) =
    ∑ x_1 in range d, ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1)) + ↑(Nat.choose (d + 1) d) * (↑d * x ^ (d - 1))
[PROOFSTEP]
rw [Nat.cast_succ, ← smul_eq_mul, ← sum_range_succ _ d, eval_monomial_one_add_sub]
[GOAL]
n : ℕ
x : ℚ
d : ℕ
hd : ∀ (m : ℕ), m < d → eval (1 + x) (bernoulli m) = eval x (bernoulli m) + ↑m * x ^ (m - 1)
nz : ↑(succ d) ≠ 0
⊢ ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) * (↑x_1 * x ^ (x_1 - 1)) =
    ∑ x_1 in range (d + 1), ↑(Nat.choose (d + 1) x_1) • (↑x_1 * x ^ (x_1 - 1))
[PROOFSTEP]
simp_rw [smul_eq_mul]
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
⊢ (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1) = PowerSeries.X * ↑(rescale t) (exp A)
[PROOFSTEP]
ext n
[GOAL]
case h
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ↑(PowerSeries.coeff A n) ((PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    ↑(PowerSeries.coeff A n) (PowerSeries.X * ↑(rescale t) (exp A))
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
⊢ ↑(PowerSeries.coeff A Nat.zero) ((PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    ↑(PowerSeries.coeff A Nat.zero) (PowerSeries.X * ↑(rescale t) (exp A))
[PROOFSTEP]
simp
  -- n ≥ 1, the coefficients is a sum to n+2, so use `sum_range_succ` to write as
    -- last term plus sum to n+1
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ↑(PowerSeries.coeff A (succ n)) ((PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    ↑(PowerSeries.coeff A (succ n)) (PowerSeries.X * ↑(rescale t) (exp A))
[PROOFSTEP]
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul, Nat.sum_antidiagonal_eq_sum_range_succ_mk,
  sum_range_succ]
  -- last term is zero so kill with `add_zero`
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A (x, succ n - x).fst) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (x, succ n - x).snd) (exp A - 1) +
      ↑(PowerSeries.coeff A (n + 1, succ n - (n + 1)).fst)
          (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (n + 1, succ n - (n + 1)).snd) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
simp only [RingHom.map_sub, tsub_self, constantCoeff_one, constantCoeff_exp, coeff_zero_eq_constantCoeff, mul_zero,
  sub_self, add_zero]
  -- Let's multiply both sides by (n+1)! (OK because it's a unit)
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ∑ x in range (n + 1),
      ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (by exact_mod_cast factorial_ne_zero (n + 1))
[GOAL]
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ ↑(n + 1)! ≠ 0
[PROOFSTEP]
exact_mod_cast factorial_ne_zero (n + 1)
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∑ x in range (n + 1),
      ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !)
[PROOFSTEP]
rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
  -- do trivial rearrangements to make RHS (n+1)*t^n
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    ↑(algebraMap ℚ A) ↑(n + 1)! * (t ^ n * ↑(algebraMap ℚ A) (1 / ↑n !))
[PROOFSTEP]
rw [mul_left_comm, ← RingHom.map_mul]
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (↑(n + 1)! * (1 / ↑n !))
[PROOFSTEP]
change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    t ^ n * ↑(algebraMap ℚ A) (↑((n + 1) * n !) * (1 / ↑n !))
[PROOFSTEP]
rw [cast_mul, mul_assoc, mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
  mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]
  -- But this is the RHS of `Polynomial.sum_bernoulli`
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      ∑ x in range (n + 1),
        ↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1) =
    ↑(aeval t) (↑(monomial n) (↑n + 1))
[PROOFSTEP]
rw [← sum_bernoulli, Finset.mul_sum, AlgHom.map_sum]
  -- and now we have to prove a sum is a sum, but all the terms are equal.
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∑ x in range (n + 1),
      ↑(algebraMap ℚ A) ↑(n + 1)! *
        (↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
          ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1)) =
    ∑ x in range (n + 1), ↑(aeval t) (↑(Nat.choose (n + 1) x) • bernoulli x)
[PROOFSTEP]
apply Finset.sum_congr rfl
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
⊢ ∀ (x : ℕ),
    x ∈ range (n + 1) →
      ↑(algebraMap ℚ A) ↑(n + 1)! *
          (↑(PowerSeries.coeff A x) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
            ↑(PowerSeries.coeff A (succ n - x)) (exp A - 1)) =
        ↑(aeval t) (↑(Nat.choose (n + 1) x) • bernoulli x)
[PROOFSTEP]
intro i hi
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ ↑(algebraMap ℚ A) ↑(n + 1)! *
      (↑(PowerSeries.coeff A i) (PowerSeries.mk fun n => ↑(aeval t) ((1 / ↑n !) • bernoulli n)) *
        ↑(PowerSeries.coeff A (succ n - i)) (exp A - 1)) =
    ↑(aeval t) (↑(Nat.choose (n + 1) i) • bernoulli i)
[PROOFSTEP]
simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi), one_div, AlgHom.map_smul,
  PowerSeries.coeff_one, coeff_exp, sub_zero, LinearMap.map_sub, Algebra.smul_mul_assoc, Algebra.smul_def,
  mul_right_comm _ ((aeval t) _), ← mul_assoc, ← RingHom.map_mul, succ_eq_add_one, ← Polynomial.C_eq_algebraMap,
  Polynomial.aeval_mul, Polynomial.aeval_C]
  -- finally cancel the Bernoulli polynomial and the algebra_map
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
hnp1 : IsUnit ↑(n + 1)!
i : ℕ
hi : i ∈ range (n + 1)
⊢ ↑(algebraMap ℚ A) (↑(n + 1)! * (↑i !)⁻¹ * (↑(n + 1 - i)!)⁻¹) * ↑(aeval t) (bernoulli i) =
    ↑(algebraMap ℚ A) (↑(n + 1)! / (↑i ! * ↑(n + 1 - i)!)) * ↑(aeval t) (bernoulli i)
[PROOFSTEP]
field_simp
