awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
⊢ LE.le (α := ℕ) (∑ m ∈ range (2 * n + 1), (2 * n).choose m) (∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2))
have h : ∀ i ∈ range (2 * n + 1), (2 * n).choose i ≤ (2 * n).choose (2 * n / 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
have inl : ∀ (h : n < k), ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
Tactic: rcases lt_or_ge n k with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
inl : ∀ (h : n < k), ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
have inr : ∀ (h : k ≤ n), ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
Tactic: rcases lt_or_ge n k with h | h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : n < k
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
have inl : Eq (α := ℕ) (∑ m ∈ Icc k n, m.choose k) 0
Tactic: rw [choose_eq_zero_of_lt (by lia), Icc_eq_empty_of_lt h, sum_empty]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : n < k
inl : Eq (α := ℕ) (∑ m ∈ Icc k n, m.choose k) 0
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
have inl₁ : Eq (α := ℕ) (∑ m ∈ ∅, m.choose k) 0
Tactic: rw [choose_eq_zero_of_lt (by lia), Icc_eq_empty_of_lt h, sum_empty]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : n < k
inl : Eq (α := ℕ) (∑ m ∈ Icc k n, m.choose k) 0
inl₁ : Eq (α := ℕ) (∑ m ∈ ∅, m.choose k) 0
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
have inl₂ : Eq (α := ℕ) 0 0
Tactic: rw [choose_eq_zero_of_lt (by lia), Icc_eq_empty_of_lt h, sum_empty]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n_1 k n : ℕ
hmn : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)
have inr : ∑ m ∈ insert (n + 1) (Ico k (n + 1)), m.choose k = (n + 1 + 1).choose (k + 1)
Tactic: rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n_1 k n : ℕ
hmn : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
inr : ∑ m ∈ insert (n + 1) (Ico k (n + 1)), m.choose k = (n + 1 + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)
have inr₁ : (n + 1).choose k + ∑ x ∈ Ico k (n + 1), x.choose k = (n + 1 + 1).choose (k + 1)
Tactic: rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n_1 k n : ℕ
hmn : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
inr : ∑ m ∈ insert (n + 1) (Ico k (n + 1)), m.choose k = (n + 1 + 1).choose (k + 1)
inr₁ : (n + 1).choose k + ∑ x ∈ Ico k (n + 1), x.choose k = (n + 1 + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)
have inr₂ : (n + 1).choose k + ∑ x ∈ Icc k n, x.choose k = (n + 1 + 1).choose (k + 1)
Tactic: rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n_1 k n : ℕ
hmn : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
inr : ∑ m ∈ insert (n + 1) (Ico k (n + 1)), m.choose k = (n + 1 + 1).choose (k + 1)
inr₁ : (n + 1).choose k + ∑ x ∈ Ico k (n + 1), x.choose k = (n + 1 + 1).choose (k + 1)
inr₂ : (n + 1).choose k + ∑ x ∈ Icc k n, x.choose k = (n + 1 + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)
have inr₃ : (n + 1).choose k + (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1)
Tactic: rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n_1 k n : ℕ
hmn : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
inr : ∑ m ∈ insert (n + 1) (Ico k (n + 1)), m.choose k = (n + 1 + 1).choose (k + 1)
inr₁ : (n + 1).choose k + ∑ x ∈ Ico k (n + 1), x.choose k = (n + 1 + 1).choose (k + 1)
inr₂ : (n + 1).choose k + ∑ x ∈ Icc k n, x.choose k = (n + 1 + 1).choose (k + 1)
inr₃ : (n + 1).choose k + (n + 1).choose (k + 1) = (n + 1 + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)
have inr₄ : (n + 1).choose k + (n + 1).choose (k + 1) = (n + 1).choose k + (n + 1).choose (k + 1)
Tactic: rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
have inr : ∑ m ∈ Icc k k, m.choose k = (k + 1).choose (k + 1)
Tactic: induction n, h using le_induction with
    | base => simp
    | succ n _ ih =>
      rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : k ≤ n
inr : ∑ m ∈ Icc k k, m.choose k = (k + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
have inr₁ : ∀ (n : ℕ),
  k ≤ n →
    ∀ (ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)),
      ∑ m ∈ Icc k (n + 1), m.choose k = (n + 1 + 1).choose (k + 1)
Tactic: induction n, h using le_induction with
    | base => simp
    | succ n _ ih =>
      rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
⊢ ∑ i ∈ range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)
have rw : Eq (α := ℕ) (∑ i ∈ Ico 0 (n + 1), (i + k).choose k) (∑ m ∈ Icc k (n + k), m.choose k)
Tactic: rw [← sum_Icc_choose, range_eq_Ico]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
⊢ Eq (α := ℕ) (∑ i ∈ Ico 0 (n + 1), (i + k).choose k) (∑ m ∈ Icc k (n + k), m.choose k)
have h : Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))
Tactic: convert! (sum_map _ (addRightEmbedding k) (·.choose k)).symm using 2
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))
have h : Icc k (n + k) = Ico (0 + k) (n + 1 + k)
Tactic: rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : Icc k (n + k) = Ico (0 + k) (n + 1 + k)
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))
have h₁ : Icc k (n + k) = Ico k (n + 1 + k)
Tactic: rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : Icc k (n + k) = Ico (0 + k) (n + 1 + k)
h₁ : Icc k (n + k) = Ico k (n + 1 + k)
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))
have h₂ : Icc k (n + k) = Ico k (n + k + 1)
Tactic: rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
h : Icc k (n + k) = Ico (0 + k) (n + 1 + k)
h₁ : Icc k (n + k) = Ico k (n + 1 + k)
h₂ : Icc k (n + k) = Ico k (n + k + 1)
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))
have h₃ : Icc k (n + k) = Icc k (n + k)
Tactic: rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)
have pos : ∀ (h : n = 0), ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
pos : ∀ (h : n = 0), ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)
have neg : ∀ (h : ¬n = 0), ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: by_cases h : n = 0
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)
have neg : HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
Tactic: apply (mul_right_inj' two_ne_zero).1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
have rw : HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), i * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i) =
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
Tactic: rw [two_mul, ← sum_flip]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
rw :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), i * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
have rw₁ : HAdd.hAdd (α := ℕ) (∑ r ∈ range (n + 1), (n - r) * n.choose (n - r)) (∑ r ∈ range (n + 1), (n - r) * n.choose (n - r)) =
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ r ∈ range (n + 1), (n - r) * n.choose (n - r))
Tactic: rw [two_mul, ← sum_flip]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i)
have h₁ : ∀ (x : ℕ) (h' : x ∈ range (n + 1)), (n - x) * n.choose (n - x) = (n - x) * n.choose x
Tactic: congr! 2 with _ h'
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
x : ℕ
h' : x ∈ range (n + 1)
⊢ (n - x) * n.choose (n - x) = (n - x) * n.choose x
have h₁ : (n - x) * n.choose x = (n - x) * n.choose x
Tactic: rw [choose_symm (mem_range_succ_iff.mp h')]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i) =
    ∑ i ∈ range (n + 1), n * n.choose i
have rw : Eq (α := ℕ) (∑ x ∈ range (n + 1), ((n - x) * n.choose x + x * n.choose x)) (∑ i ∈ range (n + 1), n * n.choose i)
Tactic: rw [← sum_add_distrib]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ Eq (α := ℕ) (∑ x ∈ range (n + 1), ((n - x) * n.choose x + x * n.choose x)) (∑ i ∈ range (n + 1), n * n.choose i)
have a : ∀ (x : ℕ) (h' : x ∈ range (n + 1)), (n - x) * n.choose x + x * n.choose x = n * n.choose x
Tactic: congr! 1 with _ h'
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
x : ℕ
h' : x ∈ range (n + 1)
⊢ (n - x) * n.choose x + x * n.choose x = n * n.choose x
have a : (n - x + x) * n.choose x = n * n.choose x
Tactic: rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
x : ℕ
h' : x ∈ range (n + 1)
a : (n - x + x) * n.choose x = n * n.choose x
⊢ (n - x) * n.choose x + x * n.choose x = n * n.choose x
have a₁ : n * n.choose x = n * n.choose x
Tactic: rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ ∑ i ∈ range (n + 1), n * n.choose i = n * HPow.hPow (α := ℕ) 2 n
have rw : n * ∑ i ∈ range (n + 1), n.choose i = n * HPow.hPow (α := ℕ) 2 n
Tactic: rw [← mul_sum, Nat.sum_range_choose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
rw : n * ∑ i ∈ range (n + 1), n.choose i = n * HPow.hPow (α := ℕ) 2 n
⊢ ∑ i ∈ range (n + 1), n * n.choose i = n * HPow.hPow (α := ℕ) 2 n
have rw₁ : n * HPow.hPow (α := ℕ) 2 n = n * HPow.hPow (α := ℕ) 2 n
Tactic: rw [← mul_sum, Nat.sum_range_choose]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ n * HPow.hPow (α := ℕ) 2 n = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have rw : n * HPow.hPow (α := ℕ) 2 n = 2 * n * HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
rw : n * HPow.hPow (α := ℕ) 2 n = 2 * n * HPow.hPow (α := ℕ) 2 (n - 1)
⊢ n * HPow.hPow (α := ℕ) 2 n = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have rw₁ : n * HPow.hPow (α := ℕ) 2 n = n * 2 * HPow.hPow (α := ℕ) 2 (n - 1)
Tactic: rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
rw : n * HPow.hPow (α := ℕ) 2 n = 2 * n * HPow.hPow (α := ℕ) 2 (n - 1)
rw₁ : n * HPow.hPow (α := ℕ) 2 n = n * 2 * HPow.hPow (α := ℕ) 2 (n - 1)
⊢ n * HPow.hPow (α := ℕ) 2 n = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have rw₂ : n * HPow.hPow (α := ℕ) 2 n = n * (2 * HPow.hPow (α := ℕ) 2 (n - 1))
Tactic: rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
rw : n * HPow.hPow (α := ℕ) 2 n = 2 * n * HPow.hPow (α := ℕ) 2 (n - 1)
rw₁ : n * HPow.hPow (α := ℕ) 2 n = n * 2 * HPow.hPow (α := ℕ) 2 (n - 1)
rw₂ : n * HPow.hPow (α := ℕ) 2 n = n * (2 * HPow.hPow (α := ℕ) 2 (n - 1))
⊢ n * HPow.hPow (α := ℕ) 2 n = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have rw₃ : n * HPow.hPow (α := ℕ) 2 n = n * HPow.hPow (α := ℕ) 2 n
Tactic: rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have i : HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) =
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
Tactic: calc
    2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
i :
  HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have i₁ : HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i) =
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i)
Tactic: calc
    2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
i :
  HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
i₁ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i)
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have i₂ : HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i) =
  ∑ i ∈ range (n + 1), n * n.choose i
Tactic: calc
    2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
i :
  HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
i₁ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i)
i₂ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i) =
    ∑ i ∈ range (n + 1), n * n.choose i
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have i₃ : ∑ i ∈ range (n + 1), n * n.choose i = n * HPow.hPow (α := ℕ) 2 n
Tactic: calc
    2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h : ¬n = 0
i :
  HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i)
i₁ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose (n - i)) (∑ i ∈ range (n + 1), i * n.choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i)
i₂ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (n + 1), (n - i) * n.choose i) (∑ i ∈ range (n + 1), i * n.choose i) =
    ∑ i ∈ range (n + 1), n * n.choose i
i₃ : ∑ i ∈ range (n + 1), n * n.choose i = n * HPow.hPow (α := ℕ) 2 n
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
have i₄ : n * HPow.hPow (α := ℕ) 2 n = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
Tactic: calc
    2 * ∑ i ∈ Finset.range (n + 1), i * n.choose i
      = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose (n - i)
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      rw [two_mul, ← sum_flip]
    _ = ∑ i ∈ Finset.range (n + 1), (n - i) * n.choose i
        + ∑ i ∈ Finset.range (n + 1), i * n.choose i := by
      congr! 2 with _ h'
      rw [choose_symm (mem_range_succ_iff.mp h')]
    _ = ∑ i ∈ Finset.range (n + 1), n * n.choose i := by
      rw [← sum_add_distrib]
      congr! 1 with _ h'
      rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]
    _ = n * 2 ^ n := by
      rw [← mul_sum, Nat.sum_range_choose]
    _ = 2 * (n * 2 ^ (n - 1)) := by
      rw [← mul_assoc, mul_comm 2 n, mul_assoc, mul_pow_sub_one h]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
⊢ ∑ i ∈ range (n + 1), k.multichoose i = (n + k).choose k
have zero : ∑ i ∈ range (n + 1), multichoose 0 i = (n + 0).choose 0
Tactic: cases k with
  | zero => simp [Finset.sum_range_succ']
  | succ k => grind [multichoose_eq, choose_symm_of_eq_add, sum_range_add_choose]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n k : ℕ
zero : ∑ i ∈ range (n + 1), multichoose 0 i = (n + 0).choose 0
⊢ ∑ i ∈ range (n + 1), k.multichoose i = (n + k).choose k
have succ : ∀ (k : ℕ), ∑ i ∈ range (n + 1), (k + 1).multichoose i = (n + (k + 1)).choose (k + 1)
Tactic: cases k with
  | zero => simp [Finset.sum_range_succ']
  | succ k => grind [multichoose_eq, choose_symm_of_eq_add, sum_range_add_choose]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n m : ℕ
hm :
  ∑ k ∈ range (m + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)
⊢ ∑ k ∈ range (m + 1 + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (m + 1) * (↑(n.choose (m + 1)) : ℤ)
have succ : HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ) +
    HPow.hPow (α := ℤ) (-1) (m + 1) * (↑(n.choose m + n.choose m.succ) : ℤ) =
  HPow.hPow (α := ℤ) (-1) (m + 1) * (↑(n.choose (m + 1)) : ℤ)
Tactic: rw [sum_range_succ, hm, choose_succ_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n m : ℕ
⊢ ∑ k ∈ range (m + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)
have zero : ∑ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
  HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(n.choose 0) : ℤ)
Tactic: induction m with
  | zero => simp
  | succ m hm =>
    rw [sum_range_succ, hm, choose_succ_succ]
    grind
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n m : ℕ
zero :
  ∑ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(n.choose 0) : ℤ)
⊢ ∑ k ∈ range (m + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)
have succ : ∀ (m : ℕ)
  (hm :
    ∑ k ∈ range (m + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
      HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)),
  ∑ k ∈ range (m + 1 + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (m + 1) * (↑(n.choose (m + 1)) : ℤ)
Tactic: induction m with
  | zero => simp
  | succ m hm =>
    rw [sum_range_succ, hm, choose_succ_succ]
    grind
Cleared hypotheses: m