R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in powerset x, f (card m) =
    ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j)

R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j) =
    ∑ m in range (card x + 1), Nat.choose (card x) m • f m
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in powerset x, f (card m) = ∑ m in range (card x + 1), Nat.choose (card x) m • f m
trans ∑ m in range (x.card + 1), ∑ j in x.powerset.filter fun z ↦ z.card = m, f j.card
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∀ (x_1 : Finset β), x_1 ∈ powerset x → card x_1 ∈ range (card x + 1)
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in powerset x, f (card m) =
    ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j)
refine' (sum_fiberwise_of_maps_to _ _).symm
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ∈ range (card x + 1)
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∀ (x_1 : Finset β), x_1 ∈ powerset x → card x_1 ∈ range (card x + 1)
intro y hy
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ≤ card x
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ∈ range (card x + 1)
rw [mem_range, Nat.lt_succ_iff]
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ card y ≤ card x
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ powerset x
⊢ card y ≤ card x
rw [mem_powerset] at hy
no goals
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ card y ≤ card x
exact card_le_of_subset hy
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = Nat.choose (card x) y • f y
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m in range (card x + 1), ∑ j in filter (fun z => card z = m) (powerset x), f (card j) =
    ∑ m in range (card x + 1), Nat.choose (card x) m • f m
refine' sum_congr rfl fun y _ ↦ _
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = ∑ _x in powersetLen y x, f y
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = Nat.choose (card x) y • f y
rw [← card_powersetLen, ← sum_const]
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
z : Finset β
hz : z ∈ powersetLen y x
⊢ f (card z) = f y
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
⊢ ∑ j in filter (fun z => card z = y) (powerset x), f (card j) = ∑ _x in powersetLen y x, f y
refine' sum_congr powersetLen_eq_filter.symm fun z hz ↦ _
no goals
R : Type ?u.207470
α : Type u_1
β : Type u_2
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (card x + 1)
z : Finset β
hz : z ∈ powersetLen y x
⊢ f (card z) = f y
rw [(mem_powersetLen.1 hz).2]