-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_powerset_apply_card {α β : Type*} [AddCommMonoid α] (f : ℕ → α) {x : Finset β} :
    ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ range (#x + 1), ∑ j ∈ filter (fun j => #j = m) x.powerset, f #j = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Tactic:
refine sum_congr rfl fun y _ ↦ ?_

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
⊢ ∑ j ∈ filter (fun j => #j = y) x.powerset, f #j = (#x).choose y • f y

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ≤ #x

Tactic:
rw [mem_powerset] at hy

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ #y ≤ #x

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ⊆ x
⊢ #y ≤ #x

Tactic:
exact card_le_card hy

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ∈ range (#x + 1)

Tactic:
rw [mem_range, Nat.lt_succ_iff]

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ≤ #x

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
z : Finset β
hz : z ∈ powersetCard y x
⊢ f #z = f y

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

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
⊢ ∑ j ∈ filter (fun j => #j = y) x.powerset, f #j = (#x).choose y • f y

Tactic:
rw [← card_powersetCard, ← sum_const]

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
⊢ ∑ j ∈ filter (fun j => #j = y) x.powerset, f #j = ∑ _x ∈ powersetCard y x, f y

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ 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

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), ∑ j ∈ filter (fun j => #j = m) x.powerset, f #j

α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ range (#x + 1), ∑ j ∈ filter (fun j => #j = m) x.powerset, f #j = ∑ m ∈ range (#x + 1), (#x).choose m • f m

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∀ i ∈ x.powerset, #i ∈ range (#x + 1)

Tactic:
intro y hy

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x y : Finset β
hy : y ∈ x.powerset
⊢ #y ∈ range (#x + 1)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), ∑ j ∈ filter (fun j => #j = m) x.powerset, f #j

Tactic:
refine (sum_fiberwise_of_maps_to ?_ _).symm

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∀ i ∈ x.powerset, #i ∈ range (#x + 1)

Proof state:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
⊢ ∑ j ∈ filter (fun j => #j = y) x.powerset, f #j = ∑ _x ∈ powersetCard y x, f y

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

Result:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
y : ℕ
x✝ : y ∈ range (#x + 1)
z : Finset β
hz : z ∈ powersetCard y x
⊢ f #z = f y