awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
⊢ Eq (α := ℤ) (∑ m ∈ range (n + 1), HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)) (if n = 0 then 1 else 0)
have zero : Eq (α := ℤ) (∑ m ∈ range (HAdd.hAdd (α := ℕ) 0 1), HPow.hPow (α := ℤ) (-1) m * (↑(Nat.choose 0 m) : ℤ))
  (if Eq (α := ℕ) 0 0 then 1 else 0)
Tactic: cases n with
  | zero => simp
  | succ n => simp [Int.alternating_sum_range_choose_eq_choose]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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)
⊢ Eq (α := ℤ) (∑ m ∈ range (n + 1), HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)) (if n = 0 then 1 else 0)
have succ : ∀ (n : ℕ),
  Eq (α := ℤ) (∑ m ∈ range (n + 1 + 1), HPow.hPow (α := ℤ) (-1) m * (↑((n + 1).choose m) : ℤ))
    (if n + 1 = 0 then 1 else 0)
Tactic: cases n with
  | zero => simp
  | succ n => simp [Int.alternating_sum_range_choose_eq_choose]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h0 : n ≠ 0
⊢ Eq (α := ℤ) (∑ m ∈ range (n + 1), HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)) 0
have rw : Eq (α := ℤ) (if n = 0 then 1 else 0) 0
Tactic: rw [Int.alternating_sum_range_choose, if_neg h0]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
n : ℕ
h0 : n ≠ 0
rw : Eq (α := ℤ) (if n = 0 then 1 else 0) 0
⊢ Eq (α := ℤ) (∑ m ∈ range (n + 1), HPow.hPow (α := ℤ) (-1) m * (↑(n.choose m) : ℤ)) 0
have rw₁ : Eq (α := ℤ) 0 0
Tactic: rw [Int.alternating_sum_range_choose, if_neg h0]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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), (#x).choose m • f m)
have trans : Eq.{u_2 + 1} (α := α) (∑ m ∈ x.powerset, f #m) (∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j)
Tactic: trans ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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)
⊢ Eq.{u_2 + 1} (α := α) (∑ m ∈ x.powerset, f #m) (∑ m ∈ range (#x + 1), (#x).choose m • f m)
have 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)
Tactic: trans ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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)
have refine : ∀ i ∈ x.powerset, #i ∈ range (#x + 1)
Tactic: refine (sum_fiberwise_of_maps_to ?_ _).symm
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ∈ range (#x + 1)
have rw : #y ≤ #x
Tactic: rw [mem_range, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ≤ #x
have hy₁ : y ⊆ x
Tactic: rw [mem_powerset] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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)
have refine : ∀ y ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = y, f #j = (#x).choose y • f y
Tactic: refine sum_congr rfl fun y _ ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
h : y ∈ range (#x + 1)
⊢ ∑ j ∈ x.powerset with #j = y, f #j = (#x).choose y • f y
have rw : Eq.{u_2 + 1} (α := α) (∑ j ∈ x.powerset with #j = y, f #j) (∑ _x ∈ powersetCard y x, f y)
Tactic: rw [← card_powersetCard, ← sum_const]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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)
have refine : ∀ (z : Finset β) (hz : z ∈ powersetCard y x), f #z = f y
Tactic: refine sum_congr powersetCard_eq_filter.symm fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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
⊢ f #z = f y
have rw : f y = f y
Tactic: rw [(mem_powersetCard.1 hz).2]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
α : Type u_2
inst : DecidableEq α
x : Finset α
⊢ Eq (α := ℤ) (∑ m ∈ x.powerset, HPow.hPow (α := ℤ) (-1) #m) (if x = ∅ then 1 else 0)
have rw : Eq (α := ℤ) (∑ m ∈ range (#x + 1), (#x).choose m • HPow.hPow (α := ℤ) (-1) m) (if x = ∅ then 1 else 0)
Tactic: rw [sum_powerset_apply_card]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ Eq (α := ℤ) (∑ m ∈ x.powerset, HPow.hPow (α := ℤ) (-1) #m) 0
have rw : Eq (α := ℤ) (if x = ∅ then 1 else 0) 0
Tactic: rw [sum_powerset_neg_one_pow_card]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ Eq (α := ℤ) (∑ m ∈ x.powerset, HPow.hPow (α := ℤ) (-1) #m) 0
have rw : Eq (α := ℤ) (if x = ∅ then 1 else 0) 0
Tactic: classical
  rw [sum_powerset_neg_one_pow_card]
  exact if_neg (nonempty_iff_ne_empty.mp h0)
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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
have 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
Tactic: rw [prod_range_succ, prod_range_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ 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)
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
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
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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
⊢ ∏ 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)
have 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)
Tactic: rw [prod_range_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ ∏ 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)
have 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))
Tactic: simp only [Nat.prod_antidiagonal_eq_prod_range_succ_mk, prod_pow_choose_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (hypothesis)
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
⊢ 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))
have this : ∀ 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
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
⊢ 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))
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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)
⊢ 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))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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)
have e_a : ∀ (i : ℕ) (hi : i ∈ range n.succ), f i (n + 1 - i) ^ n.choose i = f i (n - i + 1) ^ n.choose i
Tactic: refine prod_congr rfl fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f i (n + 1 - i) ^ n.choose i = f i (n - i + 1) ^ n.choose i
have e_a : f i (n + 1 - i) ^ n.choose i = f i (n + 1 - i) ^ n.choose i
Tactic: rw [tsub_add_eq_add_tsub (this _ hi)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
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))
have e_a : ∀ (i : ℕ) (hi : i ∈ range n.succ), f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)
Tactic: refine prod_congr rfl fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
M : Type u_2
inst : CommMonoid M
f : ℕ → ℕ → M
n : ℕ
this : ∀ i ∈ range (n + 1), i ≤ n
i : ℕ
hi : i ∈ range n.succ
⊢ f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose (n - i)
have e_a : f (i + 1) (n - i) ^ n.choose i = f (i + 1) (n - i) ^ n.choose i
Tactic: rw [choose_symm (this _ hi)]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
d n : ℕ
hn : ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)
have succ : (d + (0, n + 1).2).choose d + ∑ p ∈ @antidiagonal _ instAddMonoid _ n, (d + (p.1 + 1, p.2).2).choose d =
  (d + (n + 1) + 1).choose (d + 1)
Tactic: rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
d n : ℕ
hn : ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
succ :
  (d + (0, n + 1).2).choose d + ∑ p ∈ @antidiagonal _ instAddMonoid _ n, (d + (p.1 + 1, p.2).2).choose d =
    (d + (n + 1) + 1).choose (d + 1)
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)
have succ₁ : (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1) + 1).choose (d + 1)
Tactic: rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
d n : ℕ
hn : ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
succ :
  (d + (0, n + 1).2).choose d + ∑ p ∈ @antidiagonal _ instAddMonoid _ n, (d + (p.1 + 1, p.2).2).choose d =
    (d + (n + 1) + 1).choose (d + 1)
succ₁ : (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1) + 1).choose (d + 1)
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)
have succ₂ : (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1)).choose d + (d + (n + 1)).choose d.succ
Tactic: rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
d n : ℕ
hn : ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
succ :
  (d + (0, n + 1).2).choose d + ∑ p ∈ @antidiagonal _ instAddMonoid _ n, (d + (p.1 + 1, p.2).2).choose d =
    (d + (n + 1) + 1).choose (d + 1)
succ₁ : (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1) + 1).choose (d + 1)
succ₂ : (d + (0, n + 1).2).choose d + (d + n + 1).choose (d + 1) = (d + (n + 1)).choose d + (d + (n + 1)).choose d.succ
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)
have succ₃ : (d + n + 1).choose d + (d + n + 1).choose (d + 1) = (d + n + 1).choose d + (d + n + 1).choose d.succ
Tactic: rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
d n : ℕ
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
have zero : ∑ ij ∈ @antidiagonal _ instAddMonoid _ 0, (d + ij.2).choose d = (d + 0 + 1).choose (d + 1)
Tactic: induction n with
  | zero => simp
  | succ n hn => rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Sum (goal)
Goal:
d n : ℕ
zero : ∑ ij ∈ @antidiagonal _ instAddMonoid _ 0, (d + ij.2).choose d = (d + 0 + 1).choose (d + 1)
⊢ ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)
have succ : ∀ (n : ℕ) (hn : ∑ ij ∈ @antidiagonal _ instAddMonoid _ n, (d + ij.2).choose d = (d + n + 1).choose (d + 1)),
  ∑ ij ∈ @antidiagonal _ instAddMonoid _ (n + 1), (d + ij.2).choose d = (d + (n + 1) + 1).choose (d + 1)
Tactic: induction n with
  | zero => simp
  | succ n hn => rw [Nat.sum_antidiagonal_succ, hn, Nat.choose_succ_succ (d + (n + 1)), ← add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
m n k : ℕ
⊢ (m + n).choose k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k
have rw : (m + n).choose k = (↑((m + n).choose k) : ℕ)
Tactic: rw [coeff_X_add_one_pow, cast_id]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
m n k : ℕ
rw : (m + n).choose k = (↑((m + n).choose k) : ℕ)
⊢ (m + n).choose k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k
have rw₁ : (m + n).choose k = (m + n).choose k
Tactic: rw [coeff_X_add_one_pow, cast_id]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
m n k : ℕ
⊢ (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k =
    (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k
have rw : (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k =
  (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k
Tactic: rw [pow_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
m n k : ℕ
⊢ (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k =
    ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2
have rw : ∀ x ∈ @antidiagonal _ instAddMonoid _ k,
  (HAdd.hAdd (α := ℕ[X]) X 1 ^ m).coeff x.1 * (HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff x.2 = m.choose x.1 * n.choose x.2
Tactic: rw [coeff_mul, Finset.sum_congr rfl]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
m n k : ℕ
⊢ (m + n).choose k = ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2
have k₁ : (m + n).choose k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k
Tactic: calc
    (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
    _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
m n k : ℕ
k₁ : (m + n).choose k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k
⊢ (m + n).choose k = ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2
have k₂ : (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k
Tactic: calc
    (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
    _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
m n k : ℕ
k₁ : (m + n).choose k = (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k
k₂ :
  (HAdd.hAdd (α := ℕ[X]) X 1 ^ (m + n)).coeff k =
    (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k
⊢ (m + n).choose k = ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2
have k₃ : (HAdd.hAdd (α := ℕ[X]) X 1 ^ m * HAdd.hAdd (α := ℕ[X]) X 1 ^ n).coeff k =
  ∑ ij ∈ @antidiagonal _ instAddMonoid _ k, m.choose ij.1 * n.choose ij.2
Tactic: calc
    (m + n).choose k = ((X + 1) ^ (m + n)).coeff k := by rw [coeff_X_add_one_pow, cast_id]
    _ = ((X + 1) ^ m * (X + 1) ^ n).coeff k := by rw [pow_add]
    _ = ∑ ij ∈ antidiagonal k, m.choose ij.1 * n.choose ij.2 := by
      rw [coeff_mul, Finset.sum_congr rfl]
      simp only [coeff_X_add_one_pow, cast_id, imp_true_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
n : ℕ
⊢ ∑ i ∈ range (n + 1), HPow.hPow (β := ℕ) (n.choose i) 2 = (2 * n).choose n
have rw : Eq (α := ℕ) (∑ i ∈ range (n + 1), HPow.hPow (β := ℕ) (n.choose i) 2)
  (∑ k ∈ range n.succ, n.choose (k, n - k).1 * n.choose (k, n - k).2)
Tactic: rw [two_mul, add_choose_eq, sum_antidiagonal_eq_sum_range_succ_mk]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∑ i ∈ range (n + 1), HPow.hPow (β := ℕ) (n.choose i) 2)
    (∑ k ∈ range n.succ, n.choose (k, n - k).1 * n.choose (k, n - k).2)
have a : ∀ (x : ℕ) (h : x ∈ range n.succ), HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose (x, n - x).2
Tactic: congr! 1 with _ h
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
n x : ℕ
h : x ∈ range n.succ
⊢ HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose (x, n - x).2
have a : HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose x
Tactic: rw [choose_symm (Finset.mem_range_succ_iff.mp h), sq]
-- Lean 4 proof step from Mathlib.Data.Nat.Choose.Vandermonde (goal)
Goal:
n x : ℕ
h : x ∈ range n.succ
a : HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose x
⊢ HPow.hPow (β := ℕ) (n.choose x) 2 = n.choose (x, n - x).1 * n.choose (x, n - x).2
have a₁ : n.choose x * n.choose x = n.choose (x, n - x).1 * n.choose x
Tactic: rw [choose_symm (Finset.mem_range_succ_iff.mp h), sq]
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p n = #({x ∈ range n | p x})
have rw : (List.filter (fun (b : ℕ) ↦ decide (p b)) (List.range n)).length = #({x ∈ range n | p x})
Tactic: rw [count, List.countP_eq_length_filter]
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k : ℕ // k < n ∧ p k }
have H : ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x
Tactic: rw [count_eq_card_filter_range, Fintype.card_of_subtype]
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p n ≤ n
have rw : #({x ∈ range n | p x}) ≤ n
Tactic: rw [count_eq_card_filter_range]
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
a b : ℕ
⊢ count p (a + b) = count (fun (k : ℕ) ↦ p (k + b)) a + count p b
have rw : count (fun (k : ℕ) ↦ p (b + k)) a + count p b = count (fun (k : ℕ) ↦ p (k + b)) a + count p b
Tactic: rw [add_comm, count_add, add_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0
have rw : count (fun (k : ℕ) ↦ p (k + 1)) n + count p 1 = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0
Tactic: rw [count_add', count_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
rw : count (fun (k : ℕ) ↦ p (k + 1)) n + count p 1 = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0
⊢ count p (n + 1) = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0
have rw₁ : (count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0) = count (fun (k : ℕ) ↦ p (k + 1)) n + if p 0 then 1 else 0
Tactic: rw [count_add', count_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
⊢ m = n
have by_contra : ∀ (h : m ≠ n), False
Tactic: by_contra h : m ≠ n
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
⊢ False
have inr : ∀
  (this :
    ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) (h : m ≠ n)
      (hmn : m < n), False)
  (hmn : ¬m < n), False
Tactic: wlog hmn : m < n
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
inr :
  ∀
    (this :
      ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n)
        (h : m ≠ n) (hmn : m < n), False)
    (hmn : ¬m < n), False
⊢ False
have wlog : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) (h : m ≠ n)
  (hmn : m < n), False
Tactic: wlog hmn : m < n
Cleared hypotheses: m, n, hm, hn, heq, h
-- Lean 4 proof step from Mathlib.Data.Nat.Count (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Finite
n : ℕ
⊢ count p n ≤ #(hp.toFinset (s := setOf p))
have rw : #({x ∈ range n | p x}) ≤ #(hp.toFinset (s := setOf p))
Tactic: rw [count_eq_card_filter_range]