Theorem: chooseHalfLePowFour (FromTheBook/Ch02/Bertrand/ProdPrimes.lean)

State before:
m : ℕ
⊢ ∑ k in {m}, Nat.choose (2 * m + 1) k = ∑ k in Finset.Ico m (m + 1), Nat.choose (2 * m + 1) k
Tactic:
rw [Nat.Ico_succ_singleton]
State after:
no goals

State before:
m : ℕ
⊢ ∑ k in Finset.Ico 0 (m + 1), Nat.choose (2 * m + 1) k = ∑ k in Finset.range (m + 1), Nat.choose (2 * m + 1) k
Tactic:
rw [Finset.range_eq_Ico]
State after:
no goals