-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
a :
  HSub.hSub (α := G) (∑ a ∈ s.biUnion S, f a)
      (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (#(↑t : Finset ι) + 1)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a)) =
    HAdd.hAdd (α := G)
      (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑t : Finset ι)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a))
      (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ s.biUnion S, f a))
a₁ :
  HAdd.hAdd (α := G)
      (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑t : Finset ι)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a))
      (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ s.biUnion S, f a)) =
    ∑ t ∈ s.powerset,
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t)
        (if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a)
a₂ :
  Eq.{u_3 + 1} (α := G)
    (∑ t ∈ s.powerset,
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-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, HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((↑(S i) : Set α).indicator 1 a)) (f a))
⊢ HSub.hSub (α := G) (∑ a ∈ s.biUnion S, f a)
      (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (#(↑t : Finset ι) + 1)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a)) =
    0
have a₃ : Eq.{u_3 + 1} (α := G)
  (∑ a ∈ s.biUnion S, HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((↑(S i) : Set α).indicator 1 a)) (f a))
  (∑ a ∈ s.biUnion S,
    HSMul.hSMul (α := ℤ)
      (∏ i ∈ s, HSub.hSub (α := ℤ) ((↑(s.biUnion S) : Set α).indicator 1 a) ((↑(S i) : Set α).indicator 1 a)) (f a))
Tactic: calc
    ∑ 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
      = ∑ t : s.powerset.filter (·.Nonempty),
          (-1) ^ #t.1 • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a +
          ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ s.biUnion S, f a := by
      simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t •
          if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a := by
      rw [← sum_attach (filter ..)]; simp [sum_dite]
    _ = ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - Set.indicator (S i) 1 a : ℤ)) • f a := by
      simp only [Int.reduceNeg, prod_sub, sum_comm (s := s.biUnion S), sum_smul, mul_assoc]
      congr! with t
      split_ifs with ht
      · obtain ⟨i, hi⟩ := ht
        simp only [prod_const_one, prod_indicator_apply]
        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]
        congr
        aesop
      · obtain rfl := not_nonempty_iff_eq_empty.1 ht
        simp
    _ = ∑ a ∈ s.biUnion S, (∏ i ∈ s,
          (Set.indicator (s.biUnion S) 1 a - Set.indicator (S i) 1 a) : ℤ) • f a := by
      congr! with t; rw [Set.indicator_of_mem ‹_›, Pi.one_apply]
    _ = 0 := by
      obtain rfl | hs := s.eq_empty_or_nonempty <;>
        simp [-coe_biUnion, prod_indicator_biUnion_finset_sub_indicator, *]