awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
h : Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))
⊢ Eq (α := ℕ) (∑ i ∈ Ico 0 (n + 1), (i + k).choose k) (∑ m ∈ Icc k (n + k), m.choose k)

Tactic:
convert! (sum_map _ (addRightEmbedding k) (·.choose k)).symm using 2

Premises used: Nat.choose, Finset.sum_map, Eq.symm, addRightEmbedding
-- Module: Mathlib.Data.Nat.Choose.Sum
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)
h₃ h₄ : Icc k (n + k) = Icc k (n + k)
⊢ Icc k (n + k) = map (addRightEmbedding k) (Ico 0 (n + 1))

Tactic:
rw [map_add_right_Ico, zero_add, add_right_comm, Ico_add_one_right_eq_Icc]

Premises used: add_right_comm, zero_add, Finset.Ico_add_one_right_eq_Icc, Finset.map_add_right_Ico
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
pos : ∀ (h : n = 0), ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)
neg : ∀ (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)

Tactic:
by_cases h : n = 0
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : n = 0
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
simp [h]
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ¬n = 0
neg : HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
⊢ ∑ i ∈ range (n + 1), i * n.choose i = n * HPow.hPow (α := ℕ) 2 (n - 1)

Tactic:
apply (mul_right_inj' two_ne_zero).1

Premises used: two_ne_zero, Iff.mp, mul_right_inj'
-- Module: Mathlib.Data.Nat.Choose.Sum
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)
rw₁ 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))
⊢ 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:
rw [two_mul, ← sum_flip]

Premises used: Finset.sum_flip, two_mul
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ¬n = 0
h₁ : ∀ (x : ℕ) (h' : x ∈ range (n + 1)), (n - x) * n.choose (n - x) = (n - x) * n.choose x
⊢ 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:
congr! 2 with _ h'
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ¬n = 0
x : ℕ
h' : x ∈ range (n + 1)
h₁ h₂ : (n - x) * n.choose x = (n - x) * n.choose x
⊢ (n - x) * n.choose (n - x) = (n - x) * n.choose x

Tactic:
rw [choose_symm (mem_range_succ_iff.mp h')]

Premises used: Finset.mem_range_succ_iff, Nat.choose_symm, Iff.mp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ¬n = 0
rw : Eq (α := ℕ) (∑ x ∈ range (n + 1), ((n - x) * n.choose x + x * n.choose x)) (∑ i ∈ range (n + 1), n * n.choose 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:
rw [← sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ¬n = 0
a : ∀ (x : ℕ) (h' : x ∈ range (n + 1)), (n - x) * n.choose x + x * n.choose x = n * n.choose x
⊢ Eq (α := ℕ) (∑ x ∈ range (n + 1), ((n - x) * n.choose x + x * n.choose x)) (∑ i ∈ range (n + 1), n * n.choose i)

Tactic:
congr! 1 with _ h'
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ¬n = 0
x : ℕ
h' : x ∈ range (n + 1)
a : (n - x + x) * n.choose x = n * n.choose x
a₁ a₂ : n * n.choose x = n * n.choose x
⊢ (n - x) * n.choose x + x * n.choose x = n * n.choose x

Tactic:
rw [← add_mul, Nat.sub_add_cancel (mem_range_succ_iff.mp h')]

Premises used: add_mul, Finset.mem_range_succ_iff, Nat.sub_add_cancel, Iff.mp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h : ¬n = 0
rw : n * ∑ i ∈ range (n + 1), n.choose i = n * HPow.hPow (α := ℕ) 2 n
rw₁ rw₂ : n * HPow.hPow (α := ℕ) 2 n = n * HPow.hPow (α := ℕ) 2 n
⊢ ∑ i ∈ range (n + 1), n * n.choose i = n * HPow.hPow (α := ℕ) 2 n

Tactic:
rw [← mul_sum, Nat.sum_range_choose]

Premises used: Finset.mul_sum, Nat.sum_range_choose
-- Module: Mathlib.Data.Nat.Choose.Sum
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))
rw₃ rw₄ : n * HPow.hPow (α := ℕ) 2 n = n * HPow.hPow (α := ℕ) 2 n
⊢ 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]

Premises used: mul_assoc, mul_pow_sub_one, mul_comm, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Sum
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
i₄ : n * HPow.hPow (α := ℕ) 2 n = 2 * (n * HPow.hPow (α := ℕ) 2 (n - 1))
⊢ HMul.hMul (α := ℕ) 2 (∑ i ∈ range (n + 1), i * n.choose i) = 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]

Premises used: HMul.hMul, HSub.hSub, Finset.range, HPow.hPow, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ ∑ i ∈ range (n + 1), multichoose 0 i = (n + 0).choose 0

Tactic:
simp [Finset.sum_range_succ']

Premises used: Finset.sum_range_succ'
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
⊢ ∑ i ∈ range (n + 1), (k + 1).multichoose i = (n + (k + 1)).choose (k + 1)

Tactic:
grind [multichoose_eq, choose_symm_of_eq_add, sum_range_add_choose]

Premises used: Nat.sum_range_add_choose, Nat.multichoose_eq, Nat.choose_symm_of_eq_add
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n k : ℕ
zero : ∑ i ∈ range (n + 1), multichoose 0 i = (n + 0).choose 0
succ : ∀ (k : ℕ), ∑ i ∈ range (n + 1), (k + 1).multichoose i = (n + (k + 1)).choose (k + 1)
⊢ ∑ i ∈ range (n + 1), k.multichoose i = (n + k).choose k

Tactic:
cases k with
  | zero => simp [Finset.sum_range_succ']
  | succ k => grind [multichoose_eq, choose_symm_of_eq_add, sum_range_add_choose]

Premises used: Nat.sum_range_add_choose, Nat.multichoose_eq, Nat.zero, Nat.succ, Finset.sum_range_succ', Nat.choose_symm_of_eq_add
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ ∑ k ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (β := ℕ) (-1) 0 * (↑(n.choose 0) : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n m : ℕ
hm :
  ∑ k ∈ range (m + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)
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)) : ℤ)
⊢ ∑ k ∈ range (m + 1 + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) (m + 1) * (↑(n.choose (m + 1)) : ℤ)

Tactic:
rw [sum_range_succ, hm, choose_succ_succ]

Premises used: Nat.choose_succ_succ, Finset.sum_range_succ
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n m : ℕ
hm :
  ∑ k ∈ range (m + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)
⊢ 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:
grind
-- Module: Mathlib.Data.Nat.Choose.Sum
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) : ℤ)
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)) : ℤ)
⊢ ∑ k ∈ range (m + 1), HPow.hPow (α := ℤ) (-1) k * (↑((n + 1).choose k) : ℤ) =
    HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)

Tactic:
induction m with
  | zero => simp
  | succ m hm =>
    rw [sum_range_succ, hm, choose_succ_succ]
    grind

Premises used: Nat.choose_succ_succ, Int.succ, Nat.zero, Finset.sum_range_succ
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
⊢ Eq (α := ℤ) (∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) m * (↑(Nat.choose 0 m) : ℤ))
    (if Eq (α := ℕ) 0 0 then 1 else 0)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
⊢ Eq (α := ℤ) (∑ m ∈ range (n + 1 + 1), HPow.hPow (α := ℤ) (-1) m * (↑((n + 1).choose m) : ℤ))
    (if n + 1 = 0 then 1 else 0)

Tactic:
simp [Int.alternating_sum_range_choose_eq_choose]

Premises used: Int.alternating_sum_range_choose_eq_choose
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
zero :
  Eq (α := ℤ) (∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) m * (↑(Nat.choose 0 m) : ℤ))
    (if Eq (α := ℕ) 0 0 then 1 else 0)
succ :
  ∀ (n : ℕ),
    Eq (α := ℤ) (∑ m ∈ range (n + 1 + 1), HPow.hPow (α := ℤ) (-1) m * (↑((n + 1).choose m) : ℤ))
      (if n + 1 = 0 then 1 else 0)
⊢ Eq (α := ℤ) (∑ m ∈ range (n + 1), HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)) (if n = 0 then 1 else 0)

Tactic:
cases n with
  | zero => simp
  | succ n => simp [Int.alternating_sum_range_choose_eq_choose]

Premises used: Int.alternating_sum_range_choose_eq_choose, Int.succ, Nat.zero
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
n : ℕ
h0 : n ≠ 0
rw : Eq (α := ℤ) (if n = 0 then 1 else 0) 0
rw₁ rw₂ : Eq (α := ℤ) 0 0
⊢ Eq (α := ℤ) (∑ m ∈ range (n + 1), HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)) 0

Tactic:
rw [Int.alternating_sum_range_choose, if_neg h0]

Premises used: Int.alternating_sum_range_choose, if_neg
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
trans : Eq.{u_2 + 1} (α := α) (∑ m ∈ x.powerset, f #m) (∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j)
trans₁ :
  Eq.{u_2 + 1} (α := α) (∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j)
    (∑ m ∈ range (#x + 1), (#x).choose m • f m)
⊢ Eq.{u_2 + 1} (α := α) (∑ m ∈ x.powerset, f #m) (∑ m ∈ range (#x + 1), (#x).choose m • f m)

Tactic:
trans ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j

Premises used: Finset.range, HAdd.hAdd, Finset.card, Finset.powerset, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ Eq.{u_2 + 1} (α := α) (∑ m ∈ x.powerset, f #m) (∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j)

Tactic:
(sum_fiberwise_of_maps_to ?_ _).symm

Premises used: Finset.sum_fiberwise_of_maps_to, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
refine : ∀ i ∈ x.powerset, #i ∈ range (#x + 1)
⊢ Eq.{u_2 + 1} (α := α) (∑ m ∈ x.powerset, f #m) (∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j)

Tactic:
refine (sum_fiberwise_of_maps_to ?_ _).symm

Premises used: Finset.sum_fiberwise_of_maps_to, Eq.symm
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
rw : #y ≤ #x
⊢ #y ∈ range (#x + 1)

Tactic:
rw [mem_range, Nat.lt_succ_iff]

Premises used: Finset.mem_range, Nat.lt_succ_iff
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ y ⊆ x

Tactic:
rw [mem_powerset] at hy

Premises used: Finset.mem_powerset
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ #y ≤ #x

Tactic:
card_le_card hy

Premises used: Finset.card_le_card
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ #y ≤ #x

Tactic:
exact card_le_card hy

Premises used: Finset.card_le_card
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ Eq.{u_2 + 1} (α := α) (∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j)
    (∑ m ∈ range (#x + 1), (#x).choose m • f m)

Tactic:
sum_congr rfl fun y _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
refine : ∀ y ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = y, f #j = (#x).choose y • f y
⊢ Eq.{u_2 + 1} (α := α) (∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j)
    (∑ m ∈ range (#x + 1), (#x).choose m • f m)

Tactic:
refine sum_congr rfl fun y _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
h : y ∈ range (#x + 1)
rw : Eq.{u_2 + 1} (α := α) (∑ j ∈ x.powerset with #j = y, f #j) (∑ _x ∈ powersetCard y x, f y)
⊢ ∑ j ∈ x.powerset with #j = y, f #j = (#x).choose y • f y

Tactic:
rw [← card_powersetCard, ← sum_const]

Premises used: Finset.card_powersetCard, Finset.sum_const
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
h : y ∈ range (#x + 1)
⊢ Eq.{u_2 + 1} (α := α) (∑ j ∈ x.powerset with #j = y, f #j) (∑ _x ∈ powersetCard y x, f y)

Tactic:
sum_congr powersetCard_eq_filter.symm fun z hz ↦ ?_

Premises used: Finset.powersetCard_eq_filter, Eq.symm, Finset.sum_congr
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
h : y ∈ range (#x + 1)
refine : ∀ (z : Finset β) (hz : z ∈ powersetCard y x), f #z = f y
⊢ Eq.{u_2 + 1} (α := α) (∑ j ∈ x.powerset with #j = y, f #j) (∑ _x ∈ powersetCard y x, f y)

Tactic:
refine sum_congr powersetCard_eq_filter.symm fun z hz ↦ ?_

Premises used: Finset.powersetCard_eq_filter, Eq.symm, Finset.sum_congr
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
h : y ∈ range (#x + 1)
z : Finset β
hz : z ∈ powersetCard y x
rw rw₁ : f y = f y
⊢ f #z = f y

Tactic:
rw [(mem_powersetCard.1 hz).2]

Premises used: Finset.mem_powersetCard, And.right, Iff.mp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
inst : DecidableEq α
x : Finset α
rw : Eq (α := ℤ) (∑ m ∈ range (#x + 1), (#x).choose m • HPow.hPow (α := ℤ) (-1) m) (if x = ∅ then 1 else 0)
⊢ Eq (α := ℤ) (∑ m ∈ x.powerset, HPow.hPow (α := ℤ) (-1) #m) (if x = ∅ then 1 else 0)

Tactic:
rw [sum_powerset_apply_card]

Premises used: Finset.sum_powerset_apply_card
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
inst : DecidableEq α
x : Finset α
⊢ Eq (α := ℤ) (∑ m ∈ range (#x + 1), (#x).choose m • HPow.hPow (α := ℤ) (-1) m) (if x = ∅ then 1 else 0)

Tactic:
simp only [nsmul_eq_mul', ← card_eq_zero, Int.alternating_sum_range_choose]

Premises used: Int.alternating_sum_range_choose, nsmul_eq_mul', Finset.card_eq_zero
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
x : Finset α
h0 : x.Nonempty
rw : Eq (α := ℤ) (if x = ∅ then 1 else 0) 0
⊢ Eq (α := ℤ) (∑ m ∈ x.powerset, HPow.hPow (α := ℤ) (-1) #m) 0

Tactic:
rw [sum_powerset_neg_one_pow_card]

Premises used: Finset.sum_powerset_neg_one_pow_card
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ Eq (α := ℤ) (if x = ∅ then 1 else 0) 0

Tactic:
if_neg (nonempty_iff_ne_empty.mp h0)

Premises used: Finset.nonempty_iff_ne_empty, Iff.mp, if_neg
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ Eq (α := ℤ) (if x = ∅ then 1 else 0) 0

Tactic:
exact if_neg (nonempty_iff_ne_empty.mp h0)

Premises used: Finset.nonempty_iff_ne_empty, Iff.mp, if_neg
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
α : Type u_2
x : Finset α
h0 : x.Nonempty
rw rw₁ rw₂ : Eq (α := ℤ) (if x = ∅ then 1 else 0) 0
⊢ Eq (α := ℤ) (∑ m ∈ x.powerset, HPow.hPow (α := ℤ) (-1) #m) 0

Tactic:
classical
  rw [sum_powerset_neg_one_pow_card]
  exact if_neg (nonempty_iff_ne_empty.mp h0)

Premises used: Finset.nonempty_iff_ne_empty, Iff.mp, Finset.sum_powerset_neg_one_pow_card, if_neg
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
rw :
  (∏ x ∈ range n, f (x + 1) (n - x) ^ n.choose (x + 1)) * f (n + 1) (n - n) ^ n.choose (n + 1) * f 0 (n + 1) =
    (∏ k ∈ range n, f (k + 1) (n + 1 - (k + 1)) ^ n.choose (k + 1)) * f 0 (n + 1 - 0) ^ n.choose 0
⊢ (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i

Tactic:
rw [prod_range_succ, prod_range_succ']

Premises used: Finset.prod_range_succ', Finset.prod_range_succ
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ x ∈ range n, f (x + 1) (n - x) ^ n.choose (x + 1)) * f (n + 1) (n - n) ^ n.choose (n + 1) * f 0 (n + 1) =
    (∏ k ∈ range n, f (k + 1) (n + 1 - (k + 1)) ^ n.choose (k + 1)) * f 0 (n + 1 - 0) ^ n.choose 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i

Tactic:
have A : (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ (n.choose (i + 1))) * f 0 (n + 1) =
      ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ (n.choose i) := by
    rw [prod_range_succ, prod_range_succ']; simp
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
rw :
  (∏ k ∈ range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ (n + 1).choose (k + 1)) * f 0 (n + 1 - 0) ^ (n + 1).choose 0 =
    HMul.hMul (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
      (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i)
⊢ ∏ i ∈ range (n + 2), f i (n + 1 - i) ^ (n + 1).choose i =
    HMul.hMul (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
      (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i)

Tactic:
rw [prod_range_succ']

Premises used: Finset.prod_range_succ'
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
A :
  (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose (i + 1)) * f 0 (n + 1) =
    ∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i
⊢ (∏ k ∈ range (n + 1), f (k + 1) (n + 1 - (k + 1)) ^ (n + 1).choose (k + 1)) * f 0 (n + 1 - 0) ^ (n + 1).choose 0 =
    HMul.hMul (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
      (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i)

Tactic:
simpa [choose_succ_succ, pow_add, prod_mul_distrib, A, mul_assoc] using mul_comm _ _

Premises used: Finset.prod_mul_distrib, mul_assoc, Nat.choose_succ_succ, pow_add, mul_comm
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
simp :
  HMul.hMul (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
      (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i) =
    HMul.hMul (α := M) (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x)
      (∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x))
⊢ ∏ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 =
    HMul.hMul (α := M) (∏ ij ∈ @antidiagonal _ instAddMonoid _ n, f ij.1 (ij.2 + 1) ^ n.choose ij.1)
      (∏ ij ∈ @antidiagonal _ instAddMonoid _ n, f (ij.1 + 1) ij.2 ^ n.choose ij.2)

Tactic:
simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]

Premises used: Finset.prod_pow_choose_succ, Finset.Nat.prod_antidiagonal_eq_prod_range_succ_mk
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n i : ℕ
hi : i ∈ range (n + 1)
⊢ i ≤ n

Tactic:
simpa [Nat.lt_succ_iff] using hi

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∀ i ∈ range (n + 1), i ≤ n

Tactic:
have : ∀ i ∈ range (n + 1), i ≤ n := fun i hi ↦ by simpa [Nat.lt_succ_iff] using hi
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
e_a :
  Eq.{u_2 + 1} (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x)
e_a₁ :
  Eq.{u_2 + 1} (α := M) (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i)
    (∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x))
⊢ HMul.hMul (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
      (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i) =
    HMul.hMul (α := M) (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x)
      (∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x))

Tactic:
congr 1
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x)

Tactic:
prod_congr rfl fun i hi ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
e_a : ∀ (i : ℕ) (hi : i ∈ range n.succ), f i (n + 1 - i) ^ n.choose i = f i (n - i + 1) ^ n.choose i
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ range (n + 1), f i (n + 1 - i) ^ n.choose i)
    (∏ x ∈ range n.succ, f x (n - x + 1) ^ n.choose x)

Tactic:
refine prod_congr rfl fun i hi ↦ ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
e_a e_a₁ : f i (n + 1 - i) ^ n.choose i = f i (n + 1 - i) ^ n.choose i
⊢ f i (n + 1 - i) ^ n.choose i = f i (n - i + 1) ^ n.choose i

Tactic:
rw [tsub_add_eq_add_tsub (this _ hi)]

Premises used: tsub_add_eq_add_tsub
-- Module: Mathlib.Data.Nat.Choose.Sum
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ Eq.{u_2 + 1} (α := M) (∏ i ∈ range (n + 1), f (i + 1) (n - i) ^ n.choose i)
    (∏ x ∈ range n.succ, f (x + 1) (n - x) ^ n.choose (n - x))

Tactic:
prod_congr rfl fun i hi ↦ ?_

Premises used: Finset.prod_congr, rfl