-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
pos :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
neg :
  ∀ (ha : a ∉ ⋃ i ∈ s, S i),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
pos₁ :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
neg₁ neg₂ :
  ∀ (ha : a ∉ ⋃ i ∈ s, S i),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
pos₂ pos₃ :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Set.indicator (⋃ i ∈ s, S i) f a =
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a
pos₄ :
  ∀ (ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a),
    Set.indicator (⋃ i ∈ s, S i) f a -
        ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a =
      0
⊢ Set.indicator (⋃ i ∈ s, S i) f a =
    ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t, S i) f a

Tactic:
classical
  by_cases ha : a ∈ ⋃ i ∈ s, S i; swap
  · simp only [ha, not_false_eq_true, Set.indicator_of_notMem, Int.reduceNeg, pow_succ, mul_neg,
      mul_one, neg_smul]
    symm
    apply sum_eq_zero
    simp only [Int.reduceNeg, neg_eq_zero, mem_filter, mem_powerset, and_imp]
    intro t hts ht
    rw [Set.indicator_of_notMem]
    · simp
    · contrapose ha
      simp only [Set.mem_iInter] at ha
      rcases ht with ⟨i, hi⟩
      simp only [Set.mem_iUnion, exists_prop]
      exact ⟨i, hts hi, ha _ hi⟩
  rw [← sub_eq_zero]
  calc
    Set.indicator (⋃ i ∈ s, S i) f a - ∑ t ∈ s.powerset with t.Nonempty,
      (-1) ^ (#t + 1) • Set.indicator (⋂ i ∈ t.1, S i) f a
    _ = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a +
        ∑ t ∈ s.powerset with ¬ t.Nonempty, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a := by
      simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ, ha]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • Set.indicator (⋂ i ∈ t, S i) f a := by
      rw [sum_filter_add_sum_filter_not]
    _ = (∏ i ∈ s, (1 - Set.indicator (S i) 1 a : ℤ)) • f a := by
      simp only [Int.reduceNeg, prod_sub, prod_const_one, mul_one, sum_smul]
      congr! 1 with t
      simp only [prod_const_one, prod_indicator_apply]
      simp [Set.indicator]
    _ = 0 := by
      have : Set.indicator (⋃ i ∈ s, S i) 1 a = (1 : ℤ) := Set.indicator_of_mem ha 1
      rw [← this, prod_indicator_biUnion_sub_indicator, zero_smul]
      simp only [Set.mem_iUnion, exists_prop] at ha
      rcases ha with ⟨i, hi, -⟩
      exact ⟨i, hi⟩

Premises used: neg_smul, sub_eq_zero, Set.indicator, and_imp, pow_succ, Int.reduceNeg, Finset.sum_eq_zero, HSub.hSub, Set.mem_iUnion, neg_eq_zero, exists_prop, Set.mem_iInter, Finset.mem_powerset, Finset.prod, Finset.powerset, Finset.mem_filter, Set.indicator_of_notMem, mul_one, OfNat.ofNat, not_false_eq_true, Set.iUnion, Neg.neg, mul_neg