-- 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 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

Tactic:
congr

Result:
case pos.intro.e_s
ι : 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
⊢ t.inf' ⋯ S = filter (fun x => ∀ i ∈ t, x ∈ S i) (s.biUnion S)

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, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a = 0

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty <;>
  simp [-coe_biUnion, prod_indicator_biUnion_sub_indicator, *]

Result:
no goals

Proof state:
case a.h.e'_5.a.h.e'_5
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : α
a✝¹ : t ∈ s.biUnion S
x✝ : ι
a✝ : x✝ ∈ s
⊢ 1 = (↑(s.biUnion S)).indicator 1 t

Tactic:
rw [Set.indicator_of_mem ‹_›, Pi.one_apply]

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
⊢ ∑ 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

Tactic:
rw [← sub_eq_zero]

Result:
ι : 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 =
    0

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
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

Tactic:
simp

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 : { 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 =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a

Tactic:
rw [← sum_attach (filter ..)]

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

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) =
    ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - (↑(S i)).indicator 1 a)) • f a

Tactic:
simp only [Int.reduceNeg, mem_coe, prod_sub, sum_comm (s := s.biUnion S), sum_smul, mul_assoc]

Result:
ι : 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

Proof state:
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

Tactic:
split_ifs with ht

Result:
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

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

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 * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
simp only [prod_const_one, mul_one, prod_indicator_apply]

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 * (1 * (⋂ x ∈ t, ↑(S x)).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, (∏ i ∈ s, (1 - (↑(S i)).indicator 1 a)) • f a =
    ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a

Tactic:
congr! with t

Result:
case a.h.e'_5.a.h.e'_5
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : DecidableEq α
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Finset α
f : α → G
t : α
a✝¹ : t ∈ s.biUnion S
x✝ : ι
a✝ : x✝ ∈ s
⊢ 1 = (↑(s.biUnion S)).indicator 1 t

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

Tactic:
simp [sum_dite, filter_eq', sum_attach]

Result:
no goals

Proof state:
case pos.intro.e_s
ι : 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
⊢ t.inf' ⋯ S = filter (fun x => ∀ i ∈ t, x ∈ S i) (s.biUnion S)

Tactic:
aesop

Result:
no goals