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))
k : ℕ
⊢ ↑derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k
simp_rw [bernoulli, derivative_sum, derivative_monomial, Nat.sub_sub, Nat.add_sub_add_right]
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))
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))
rw [range_add_one, sum_insert not_mem_range_self, tsub_self, cast_zero, MulZeroClass.mul_zero,
  map_zero, zero_add, mul_sum]
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))
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))
refine' sum_congr (by rfl) fun m _ => _
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))
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))
conv_rhs => rw [← Nat.cast_one, ← Nat.cast_add, ← C_eq_nat_cast, C_mul_monomial, mul_comm]
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)))
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))
rw [mul_assoc, mul_assoc, ← Nat.cast_mul, ← Nat.cast_mul]
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)
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)))
congr 3
no goals
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)
rw [(choose_mul_succ_eq k m).symm, mul_comm]
no goals
k : ℕ
⊢ range (k + 1) = range (k + 1)
rfl