-- Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
theorem inclusion_exclusion_sum_biUnion (s : Finset ι) (S : ι → Finset α) (f : α → G) :
    ∑ a ∈ s.biUnion S, f a = ∑ t : s.powerset.filter (·.Nonempty),
      (-1) ^ (#t.1 + 1) • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a

Proof state:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
obtain rfl := not_nonempty_iff_eq_empty.1 ht

Result:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
a✝ : ∅ ∈ s.powerset
ht : ¬∅.Nonempty
⊢ (-1) ^ #∅ • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #∅ * ((∏ i ∈ s \ ∅, 1) * ∏ i ∈ ∅, (↑(S i)).indicator 1 x)) • f x

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, f a -
      ∑ t : { x // x ∈ filter (fun x => x.Nonempty) s.powerset }, (-1) ^ (#↑t + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a =
    ∑ t : { x // x ∈ filter (fun x => x.Nonempty) s.powerset }, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a +
      ∑ t ∈ filter (fun x => ¬x.Nonempty) s.powerset, (-1) ^ #t • ∑ a ∈ s.biUnion S, f a

Tactic:
simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
⊢ (∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a) =
    ∑ y ∈ s.powerset, ∑ x ∈ s.biUnion S, ((-1) ^ #y * ((∏ i ∈ s \ y, 1) * ∏ i ∈ y, (↑(S i)).indicator 1 x)) • f x

Tactic:
congr! with t

Result:
case a
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
⊢ ((-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a) =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Proof state:
case pos.intro
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ⋯ S, f a = ∑ x ∈ s.biUnion S, ((-1) ^ #t * (1 * (⋂ x ∈ t, ↑(S x)).indicator 1 x)) • f x

Tactic:
simp only [smul_sum, Set.indicator, Set.mem_iInter, mem_coe, Pi.one_apply, mul_ite, mul_one,
  mul_zero, ite_smul, zero_smul, sum_ite, not_forall, sum_const_zero, add_zero]

Result:
case pos.intro
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ ∑ x ∈ t.inf' ⋯ S, (-1) ^ #t • f x = ∑ x ∈ filter (fun x => ∀ i ∈ t, x ∈ S i) (s.biUnion S), (-1) ^ #t • f x

Proof state:
case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
ht : t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ht S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
obtain ⟨i, hi⟩ := ht

Result:
case pos.intro
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ⋯ S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x