awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
e_a :
  x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    y * (x ^ i.succ * y ^ (n - i.succ) * (↑(n.choose i.succ) : R))

Tactic:
rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]

Premises used: Commute.pow_right, mul_assoc, Commute.symm, Nat.succ, Commute.eq
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
pos :
  ∀ (h_eq : i = n),
    x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
      x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg :
  ∀ (h_eq : ¬i = n),
    x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
      x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)

Tactic:
by_cases h_eq : i = n
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : i = n
pos :
  x ^ n.succ * y ^ (n.succ - n.succ) * (↑(n.choose n.succ) : R) =
    x ^ n.succ * y * y ^ (n - n.succ) * (↑(n.choose n.succ) : R)
pos₁ : x ^ n.succ * y ^ (n.succ - n.succ) * (↑0 : R) = x ^ n.succ * y * y ^ (n - n.succ) * (↑0 : R)
pos₂ : x ^ n.succ * y ^ (n.succ - n.succ) * 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
pos₃ : 0 = x ^ n.succ * y * y ^ (n - n.succ) * 0
pos₄ pos₅ : Eq.{u_1 + 1} (α := R) 0 0
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)

Tactic:
rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, Nat.cast_zero, Nat.choose_succ_self
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
neg :
  x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)

Tactic:
rw [succ_sub (lt_of_le_of_ne h_le h_eq)]

Premises used: Nat.succ_sub, lt_of_le_of_ne
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n_1 : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
neg :
  x ^ i.succ * (y * y ^ (n - i.succ)) * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₁ :
  x ^ i.succ * (y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₂ :
  x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)
neg₃ :
  x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
    x ^ i.succ * y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))
neg₄ neg₅ :
  x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R))) =
    x ^ i.succ * (y * (y ^ (n - i.succ) * (↑(n.choose i.succ) : R)))
⊢ x ^ i.succ * y ^ (n - i.succ).succ * (↑(n.choose i.succ) : R) =
    x ^ i.succ * y * y ^ (n - i.succ) * (↑(n.choose i.succ) : R)

Tactic:
rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
⊢ ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ

Tactic:
have h_middle :
      ∀ n i : ℕ, i ∈ range n.succ → (t n.succ i.succ) = x * t n i + y * t n i.succ := by
    intro n i h_mem
    have h_le : i ≤ n := le_of_lt_succ (mem_range.mp h_mem)
    dsimp only [t]
    rw [choose_succ_succ, cast_add, mul_add]
    congr 1
    · rw [pow_succ' x, succ_sub_succ, mul_assoc, mul_assoc, mul_assoc]
    · rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]
      by_cases h_eq : i = n
      · rw [h_eq, choose_succ_self, cast_zero, mul_zero, mul_zero]
      · rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
        rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = t 0 0
⊢ HPow.hPow (β := ℕ) (x + y) 0 = ∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), t 0 m

Tactic:
rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]

Premises used: zero_add, pow_zero, Finset.sum_empty, Finset.sum_range_succ, Finset.range_zero
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
⊢ 1 = t 0 0

Tactic:
dsimp only [t]
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : 1 = 1 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)
zero₁ : 1 = HMul.hMul (α := R) 1 1 * (↑(Nat.choose 0 0) : R)
zero₂ : 1 = HMul.hMul (α := R) 1 1 * (↑1 : R)
zero₃ : 1 = HMul.hMul (α := R) 1 1 * 1
zero₄ : 1 = HMul.hMul (α := R) 1 1
zero₅ zero₆ : Eq.{u_1 + 1} (α := R) 1 1
⊢ 1 = HPow.hPow (β := ℕ) x 0 * y ^ HSub.hSub (α := ℕ) 0 0 * (↑(Nat.choose 0 0) : R)

Tactic:
rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]

Premises used: pow_zero, mul_one, Nat.cast_one, Nat.choose_self
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
⊢ HAdd.hAdd (α := R) (∑ i ∈ range (n + 1), x * t n i) (∑ i ∈ range (n + 1), y * t n i) =
    ∑ x_1 ∈ range n.succ, x * t n x_1 + (∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1))

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
n : ℕ
ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m
succ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)
succ₁ : ∑ k ∈ range n, y * t n (k + 1) + y * t n 0 = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₂ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * t n n.succ + y ^ (n + 1)
succ₃ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * 0 + y ^ (n + 1)
succ₄ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = HAdd.hAdd (α := R) (∑ x ∈ range n, y * t n x.succ) 0 + y ^ (n + 1)
succ₅ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y ^ (n + 1)
succ₆ succ₇ : ∑ k ∈ range n, y * t n (k + 1) + y * y ^ n = ∑ x ∈ range n, y * t n x.succ + y * y ^ n
⊢ ∑ i ∈ range (n + 1), y * t n i = ∑ x ∈ range n.succ, y * t n x.succ + y ^ (n + 1)

Tactic:
rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']

Premises used: MulZeroClass.mul_zero, add_zero, Finset.sum_range_succ', Finset.sum_range_succ, pow_succ'
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
t : ℕ → ℕ → R := fun (n m : ℕ) ↦ x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
zero : HPow.hPow (β := ℕ) (x + y) 0 = ∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), t 0 m
succ :
  ∀ (n : ℕ) (ih : (x + y) ^ n = ∑ m ∈ range (n + 1), t n m), (x + y) ^ (n + 1) = ∑ m ∈ range (n + 1 + 1), t (n + 1) m
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), t n m

Tactic:
induction n with
  | zero =>
    rw [pow_zero, sum_range_succ, range_zero, sum_empty, zero_add]
    dsimp only [t]
    rw [pow_zero, pow_zero, choose_self, cast_one, mul_one, mul_one]
  | succ n ih =>
    rw [sum_range_succ', h_first, sum_congr rfl (h_middle n), sum_add_distrib, add_assoc,
      pow_succ' (x + y), ih, add_mul, mul_sum, mul_sum]
    congr 1
    rw [sum_range_succ', sum_range_succ, h_first, h_last, mul_zero, add_zero, _root_.pow_succ']

Premises used: add_mul, Finset.mul_sum, Finset.sum_add_distrib, add_assoc, zero_add, pow_zero, MulZeroClass.mul_zero, HAdd.hAdd, Nat.zero, Finset.sum_empty, mul_one, add_zero, Nat.succ, Nat.cast_one, Finset.sum_range_succ', Finset.sum_range_succ, Finset.sum_congr, Nat.choose_self, pow_succ', rfl, Finset.range_zero
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : Semiring R
x y : R
h : Commute x y
n : ℕ
simp_rw : (x + y) ^ n = ∑ k ∈ range n.succ, n.choose k • (x ^ k * y ^ (n - k))
simp_rw₁ : (x + y) ^ n = ∑ x_1 ∈ range n.succ, (↑(n.choose x_1) : R) * (x ^ x_1 * y ^ (n - x_1))
simp_rw₂ : (x + y) ^ n = ∑ x_1 ∈ range n.succ, x ^ x_1 * y ^ (n - x_1) * (↑(n.choose x_1) : R)
⊢ (x + y) ^ n = ∑ m ∈ @antidiagonal _ instAddMonoid _ n, n.choose m.1 • (x ^ m.1 * y ^ m.2)

Tactic:
simp_rw [Nat.sum_antidiagonal_eq_sum_range_succ fun m p ↦ n.choose m • (x ^ m * y ^ p),
    nsmul_eq_mul, cast_comm, h.add_pow]

Premises used: Nat.cast_comm, Finset.Nat.sum_antidiagonal_eq_sum_range_succ, Nat.choose, HMul.hMul, Commute.add_pow, HPow.hPow, nsmul_eq_mul, HSMul.hSMul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommSemiring R
x y : R
n : ℕ
⊢ (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * (↑(n.choose m) : R)

Tactic:
(Commute.all x y).add_pow n

Premises used: Commute.add_pow, Commute.all
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R) (∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R))
    (∑ m ∈ range (n + 1), HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R))
⊢ (x - y) ^ n = ∑ m ∈ range (n + 1), HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)

Tactic:
rw [sub_eq_add_neg, add_pow]

Premises used: sub_eq_add_neg, add_pow
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n : ℕ
a :
  ∀ (m : ℕ) (hm : m ∈ range (n + 1)),
    x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R) =
      HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R))
    (∑ m ∈ range (n + 1), HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R))

Tactic:
congr! 1 with m hm
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m < n + 1

Tactic:
rw [mem_range] at hm

Premises used: Finset.mem_range
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m < n + 1
⊢ n + m = n - m + 2 * m

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m < n + 1
⊢ HPow.hPow (α := R) (-1) (n - m) = HPow.hPow (α := R) (-1) (n + m)

Tactic:
simp [show n + m = n - m + 2 * m by lia, pow_add]

Premises used: pow_add
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ HPow.hPow (α := R) (-1) (n - m) = HPow.hPow (α := R) (-1) (n + m)

Tactic:
have : (-1 : R) ^ (n - m) = (-1) ^ (n + m) := by
    rw [mem_range] at hm
    simp [show n + m = n - m + 2 * m by lia, pow_add]
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : HPow.hPow (α := R) (-1) (n - m) = HPow.hPow (α := R) (-1) (n + m)
a :
  x ^ m * (HPow.hPow (α := R) (-1) (n + m) * y ^ (n - m)) * (↑(n.choose m) : R) =
    HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)
⊢ x ^ m * (-y) ^ (n - m) * (↑(n.choose m) : R) =
    HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)

Tactic:
rw [neg_pow, this]

Premises used: neg_pow
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
R : Type u_1
inst : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : HPow.hPow (α := R) (-1) (n - m) = HPow.hPow (α := R) (-1) (n + m)
⊢ x ^ m * (HPow.hPow (α := R) (-1) (n + m) * y ^ (n - m)) * (↑(n.choose m) : R) =
    HPow.hPow (α := R) (-1) (m + n) * x ^ m * y ^ (n - m) * (↑(n.choose m) : R)

Tactic:
ring
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ ∑ m ∈ range (n + 1), HPow.hPow (α := ℕ) 1 m * HPow.hPow (α := ℕ) 1 (n - m) * (↑(n.choose m) : ℕ) =
    HAdd.hAdd (α := ℕ) 1 1 ^ n

Tactic:
have := (add_pow 1 1 n).symm
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
this :
  ∑ m ∈ range (n + 1), HPow.hPow (α := ℕ) 1 m * HPow.hPow (α := ℕ) 1 (n - m) * (↑(n.choose m) : ℕ) =
    HAdd.hAdd (α := ℕ) 1 1 ^ n
⊢ ∑ m ∈ range (n + 1), n.choose m = HPow.hPow (α := ℕ) 2 n

Tactic:
simpa [one_add_one_eq_two] using this

Premises used: one_add_one_eq_two
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m i : ℕ
hi : i ∈ range (m + 1)
linarith :
  2 * m + 1 < i →
    HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 0 (↑m : ℤ) + (HMul.hMul (α := ℤ) 2 (↑m : ℤ) + 1 + 1 - (↑i : ℤ)) +
        (HAdd.hAdd (α := ℤ) (↑i : ℤ) 1 - HAdd.hAdd (α := ℤ) (↑m : ℤ) 1) =
      0
linarith₁ : 2 * m + 1 < i → GT.gt (α := ℤ) 2 0
⊢ i ≤ 2 * m + 1

Tactic:
linarith [mem_range.1 hi]

Premises used: Finset.mem_range, Iff.mp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
rw :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
      (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i))
rw₁ rw₂ :
  HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (m + 1), (2 * m + 1).choose i) =
    HAdd.hAdd (α := ℕ) (∑ 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]

Premises used: two_mul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ 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:
lia
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
rw :
  HAdd.hAdd (α := ℕ) (∑ 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) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i) (∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i)
⊢ HAdd.hAdd (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
      (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) =
    HAdd.hAdd (α := ℕ) (∑ 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 lia)]

Premises used: Finset.range_eq_Ico, Finset.sum_Ico_reflect
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
e_a : 2 * m + 1 + 1 - (m + 1) = m + 1
⊢ HAdd.hAdd (α := ℕ) (∑ 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) =
    HAdd.hAdd (α := ℕ) (∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i) (∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i)

Tactic:
congr
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ 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:
lia
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ 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:
lia
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
rw : 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 2 ^ m = 2 * HPow.hPow (α := ℕ) 4 m
⊢ HPow.hPow (α := ℕ) 2 (2 * m + 1) = 2 * HPow.hPow (α := ℕ) 4 m

Tactic:
rw [pow_succ, pow_mul, mul_comm]

Premises used: pow_succ, pow_mul, mul_comm
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
m : ℕ
this : Eq (α := ℕ) (∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i)) (∑ i ∈ range (m + 1), (2 * m + 1).choose i)
⊢ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 2 ^ m = 2 * HPow.hPow (α := ℕ) 4 m

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n x : ℕ
h : x ∈ range (n + 1)
⊢ 0 ≤ (2 * n + 1).choose x

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i

Tactic:
have t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i :=
    single_le_sum (fun x _ ↦ by lia) (self_mem_range_succ n)
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i
⊢ (2 * n + 1).choose n ≤ HPow.hPow (α := ℕ) 4 n

Tactic:
simpa [sum_range_choose_halfway n] using t

Premises used: Nat.sum_range_choose_halfway
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ HPow.hPow (α := ℕ) 4 n = HAdd.hAdd (α := ℕ) 1 1 ^ (2 * n)

Tactic:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℕ) 1 1 ^ (2 * n) = ∑ m ∈ range (2 * n + 1), (2 * n).choose m

Tactic:
simp [-Nat.reduceAdd, add_pow]

Premises used: Nat.reduceAdd, add_pow
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ∀ i ∈ range (2 * n + 1), (2 * n).choose i ≤ (2 * n).choose (2 * n / 2)
⊢ LE.le (α := ℕ) (∑ m ∈ range (2 * n + 1), (2 * n).choose m) (∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2))

Tactic:
gcongr
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n i : ℕ
h : i ∈ range (2 * n + 1)
⊢ (2 * n).choose i ≤ (2 * n).choose (2 * n / 2)

Tactic:
apply choose_le_middle

Premises used: Nat.choose_le_middle
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ ∑ x ∈ range (2 * n + 1), (2 * n).choose (2 * n / 2) = (2 * n + 1) * (2 * n).choose n

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
inl : ∀ (h : n < k), ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
inr : ∀ (h : k ≤ n), ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
rcases lt_or_ge n k with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
h : n < k
⊢ n + 1 < k + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
h : n < k
inl : Eq (α := ℕ) (∑ m ∈ Icc k n, m.choose k) 0
inl₁ : Eq (α := ℕ) (∑ m ∈ ∅, m.choose k) 0
inl₂ inl₃ : Eq (α := ℕ) 0 0
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
rw [choose_eq_zero_of_lt (by lia), Icc_eq_empty_of_lt h, sum_empty]

Premises used: Finset.Icc_eq_empty_of_lt, Nat.choose_eq_zero_of_lt, Finset.sum_empty
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
⊢ ∑ m ∈ Icc k k, m.choose k = (k + 1).choose (k + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n_1 k n : ℕ
hmn : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ k ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n_1 k n : ℕ
hmn : k ≤ n
ih : ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)
⊢ n + 1 ∉ Ico k (n + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Sum
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)
inr₄ inr₅ : (n + 1).choose k + (n + 1).choose (k + 1) = (n + 1).choose k + (n + 1).choose (k + 1)
⊢ ∑ m ∈ Icc 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)]

Premises used: Finset.Ico_insert_right, Finset.Ico_add_one_right_eq_Icc, HAdd.hAdd, Nat.choose_succ_succ', Finset.sum_insert, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
h : k ≤ n
inr : ∑ m ∈ Icc k k, m.choose k = (k + 1).choose (k + 1)
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)
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 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)]

Premises used: Finset.Ico_insert_right, Finset.Ico_add_one_right_eq_Icc, HAdd.hAdd, Nat.choose_succ_succ', Finset.sum_insert, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
rw : Eq (α := ℕ) (∑ i ∈ Ico 0 (n + 1), (i + k).choose k) (∑ m ∈ Icc k (n + k), m.choose k)
⊢ ∑ i ∈ range (n + 1), (i + k).choose k = (n + k + 1).choose (k + 1)

Tactic:
rw [← sum_Icc_choose, range_eq_Ico]

Premises used: Nat.sum_Icc_choose, Finset.range_eq_Ico
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
⊢ Eq (α := ℕ) (∑ x ∈ Ico 0 (n + 1), choose ((addRightEmbedding k : (a : ℕ) → ℕ) x) k)
    (∑ x ∈ map (addRightEmbedding k) (Ico 0 (n + 1)), x.choose k)

Tactic:
(sum_map _ (addRightEmbedding k) (·.choose k)).symm

Premises used: Nat.choose, Finset.sum_map, Eq.symm, addRightEmbedding