no goals
R : Type ?u.210079
α : Type u_1
x : Finset α
h0 : Finset.Nonempty x
⊢ ∑ m in powerset x, (-1) ^ card m = 0
classical
  rw [sum_powerset_neg_one_pow_card, if_neg]
  rw [← Ne.def, ← nonempty_iff_ne_empty]
  apply h0
case hnc
R : Type ?u.210079
α : Type u_1
x : Finset α
h0 : Finset.Nonempty x
⊢ ¬x = ∅
R : Type ?u.210079
α : Type u_1
x : Finset α
h0 : Finset.Nonempty x
⊢ ∑ m in powerset x, (-1) ^ card m = 0
rw [sum_powerset_neg_one_pow_card, if_neg]
case hnc
R : Type ?u.210079
α : Type u_1
x : Finset α
h0 : Finset.Nonempty x
⊢ Finset.Nonempty x
case hnc
R : Type ?u.210079
α : Type u_1
x : Finset α
h0 : Finset.Nonempty x
⊢ ¬x = ∅
rw [← Ne.def, ← nonempty_iff_ne_empty]
no goals
case hnc
R : Type ?u.210079
α : Type u_1
x : Finset α
h0 : Finset.Nonempty x
⊢ Finset.Nonempty x
apply h0