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)))
n : ℕ
⊢ bernoulli n = ∑ i in range (n + 1), ↑(monomial i) (_root_.bernoulli (n - i) * ↑(Nat.choose n i))
rw [← sum_range_reflect, add_succ_sub_one, add_zero, bernoulli]
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)))
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)))
apply sum_congr rfl
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)))
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)))
rintro x hx
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)))
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)))
rw [mem_range_succ_iff] at hx
no goals
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)))
rw [choose_symm hx, tsub_tsub_cancel_of_le hx]