-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_range_choose_halfway (m : ℕ) : (∑ i ∈ range (m + 1), (2 * m + 1).choose i) = 4 ^ m :=
  have : (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) =
      ∑ i ∈ range (m + 1), (2 * m + 1).choose i :=
    sum_congr rfl fun i hi ↦ choose_symm <| by linarith [mem_range.1 hi]
  mul_right_injective₀ two_ne_zero <|
    calc
      (2 * ∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
          (∑ i ∈ range (m + 1), (2 * m + 1).choose i) +
            ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)

Proof state:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 ^ (2 * m + 1) = 2 * 4 ^ m

Tactic:
rw [pow_succ, pow_mul, mul_comm]

Result:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m

Proof state:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ m + 1 ≤ 2 * m + 1 + 1

Tactic:
omega

Result:
no goals

Proof state:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ m + 1 ≤ 2 * m + 2

Tactic:
omega

Result:
no goals

Proof state:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * ∑ i ∈ range (m + 1), (2 * m + 1).choose i =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)

Tactic:
rw [two_mul, this]

Result:
no goals

Proof state:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * (2 ^ 2) ^ m = 2 * 4 ^ m

Tactic:
rfl

Result:
no goals

Proof state:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Tactic:
rw [range_eq_Ico, sum_Ico_reflect _ _ (by omega)]

Result:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i +
      ∑ j ∈ Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), (2 * m + 1).choose j =
    ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Proof state:
case e_a.e_s.e_a
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1

Tactic:
omega

Result:
no goals

Proof state:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i +
      ∑ j ∈ Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), (2 * m + 1).choose j =
    ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Tactic:
congr

Result:
case e_a.e_s.e_a
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ 2 * m + 1 + 1 - (m + 1) = m + 1

Proof state:
m i : ℕ
hi : i ∈ range (m + 1)
⊢ i ≤ 2 * m + 1

Tactic:
linarith [mem_range.1 hi]

Result:
no goals