awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
a₁ :
  ∀ t ∈ s.powerset,
    HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a =
      (HPow.hPow (α := ℤ) (-1) #t * ∏ i ∈ t, (S i).indicator 1 a) • f a
⊢ Eq.{u_3 + 1} (α := G) (∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
    (∑ i ∈ s.powerset, (HPow.hPow (α := ℤ) (-1) #i * ∏ i ∈ i, (S i).indicator 1 a) • f a)

Tactic:
congr! 1 with t
-- 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 : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
t : Finset ι
h : t ∈ s.powerset
a₁ :
  HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a =
    (HPow.hPow (α := ℤ) (-1) #t * Set.indicator (⋂ i ∈ t, S i) 1 a) • f a
⊢ HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a =
    (HPow.hPow (α := ℤ) (-1) #t * ∏ i ∈ t, (S i).indicator 1 a) • f a

Tactic:
simp only [prod_const_one, prod_indicator_apply]

Premises used: prod_indicator_apply, Finset.prod_const_one
-- 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 : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
t : Finset ι
h : t ∈ s.powerset
⊢ HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a =
    (HPow.hPow (α := ℤ) (-1) #t * Set.indicator (⋂ i ∈ t, S i) 1 a) • f a

Tactic:
simp [Set.indicator]

Premises used: Set.indicator
-- 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 : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
⊢ Eq (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) 1

Tactic:
have : Set.indicator (⋃ i ∈ s, S i) 1 a = (1 : ℤ) := Set.indicator_of_mem ha 1
-- 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 : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
this : Eq (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) 1
hs : s.Nonempty
⊢ HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((S i).indicator 1 a)) (f a) = 0

Tactic:
rw [← this, prod_indicator_biUnion_sub_indicator, zero_smul]

Premises used: zero_smul, Finset.prod_indicator_biUnion_sub_indicator
-- 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 : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
this : Eq (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) 1
⊢ ∃ i ∈ s, a ∈ S i

Tactic:
simp only [Set.mem_iUnion, exists_prop] at ha

Premises used: Set.mem_iUnion, exists_prop
-- 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 : α
this : Eq (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) 1
ha : ∃ i ∈ s, a ∈ S i
hs : ∀ (i : ι) (hi : i ∈ s), s.Nonempty
⊢ s.Nonempty

Tactic:
rcases ha with ⟨i, hi, -⟩
-- 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 : α
this : Eq (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) 1
i : ι
hi : i ∈ s
⊢ s.Nonempty

Tactic:
⟨i, hi⟩

Premises used: Exists.intro, Finset.Nonempty
-- 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 : α
this : Eq (α := ℤ) (Set.indicator (⋃ i ∈ s, S i) 1 a) 1
i : ι
hi : i ∈ s
⊢ s.Nonempty

Tactic:
exact ⟨i, hi⟩
-- 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 : α
ha : Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
i :
  Set.indicator (⋃ i ∈ s, S i) f a -
      ∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • Set.indicator (⋂ i ∈ t.val, S i) f a =
    HAdd.hAdd (α := G) (∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
i₁ :
  HAdd.hAdd (α := G) (∑ t ∈ s.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
      (∑ t ∈ s.powerset with ¬t.Nonempty, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a) =
    ∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a
i₂ :
  ∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a =
    HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((S i).indicator 1 a)) (f a)
i₃ : HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((S i).indicator 1 a)) (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 =
    0

Tactic:
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: Set.indicator, HSub.hSub, Finset.prod, Finset.powerset, OfNat.ofNat, Set.iUnion, Neg.neg
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
inst : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
⊢ Eq (α := ℤ)
    (∏ i ∈ s, HSub.hSub (α := ℤ) (Set.indicator (⋃ i ∈ s, (↑(S i) : Set α)) 1 a) ((↑(S i) : Set α).indicator 1 a)) 0

Tactic:
prod_indicator_biUnion_sub_indicator hs (fun i ↦ S i) a

Premises used: Finset.prod_indicator_biUnion_sub_indicator
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
inst : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
h : ∀ x ∈ s, (↑(s.biUnion S) : Set α) = ⋃ i ∈ s, (↑(S i) : Set α)
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) ((↑(s.biUnion S) : Set α).indicator 1 a) ((↑(S i) : Set α).indicator 1 a)) 0

Tactic:
convert! prod_indicator_biUnion_sub_indicator hs (fun i ↦ S i) a

Premises used: Finset.prod_indicator_biUnion_sub_indicator
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
inst : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
x : ι
h : x ∈ s
⊢ (↑(s.biUnion S) : Set α) = ⋃ i ∈ s, (↑(S i) : Set α)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
rw :
  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
⊢ Eq.{u_3 + 1} (α := 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))

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ 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))

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

Premises used: pow_succ, sub_eq_neg_add, Finset.filter_eq', Finset.sum_neg_distrib
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
rw :
  HAdd.hAdd (α := G)
      (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑t : Finset ι)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a))
      (∑ x ∈ {x ∈ s.powerset | ¬x.Nonempty}.attach,
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑x : Finset ι)) (∑ 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)
⊢ 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)

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

Premises used: Finset.sum_attach, Finset.filter
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ HAdd.hAdd (α := G)
      (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑t : Finset ι)) (∑ a ∈ (↑t : Finset ι).inf' ⋯ S, f a))
      (∑ x ∈ {x ∈ s.powerset | ¬x.Nonempty}.attach,
        HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑x : Finset ι)) (∑ 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)

Tactic:
simp [sum_dite]

Premises used: Finset.sum_dite
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
simp :
  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))
    (∑ y ∈ s.powerset,
      ∑ x ∈ s.biUnion S,
        (HPow.hPow (α := ℤ) (-1) #y * HMul.hMul (α := ℤ) (∏ i ∈ s \ y, 1) (∏ i ∈ y, (↑(S i) : Set α).indicator 1 x)) •
          f x)
⊢ 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))

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

Premises used: Finset.sum_smul, Finset.prod_sub, Int.reduceNeg, mul_assoc, Finset.sum_comm
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
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) =
      ∑ x ∈ s.biUnion S,
        (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) •
          f x
⊢ 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))
    (∑ y ∈ s.powerset,
      ∑ x ∈ s.biUnion S,
        (HPow.hPow (α := ℤ) (-1) #y * HMul.hMul (α := ℤ) (∏ i ∈ s \ y, 1) (∏ i ∈ y, (↑(S i) : Set α).indicator 1 x)) •
          f x)

Tactic:
congr! with t
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
pos :
  ∀ (ht : t.Nonempty),
    HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' ht S, f a) =
      ∑ x ∈ s.biUnion S,
        (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) •
          f x
neg :
  ∀ (ht : ¬t.Nonempty),
    HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ s.biUnion S, f a) =
      ∑ x ∈ s.biUnion S,
        (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) •
          f x
⊢ 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) =
    ∑ x ∈ s.biUnion S,
      (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) • f x

Tactic:
split_ifs with ht
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
ht : t.Nonempty
pos :
  ∀ (i : ι) (hi : i ∈ t),
    HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' ⋯ S, f a) =
      ∑ x ∈ s.biUnion S,
        (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) •
          f x
⊢ HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' ht S, f a) =
    ∑ x ∈ s.biUnion S,
      (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) • f x

Tactic:
obtain ⟨i, hi⟩ := ht
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
i : ι
hi : i ∈ t
pos :
  HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' ⋯ S, f a) =
    ∑ x ∈ s.biUnion S,
      (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) 1 (Set.indicator (⋂ x ∈ t, (↑(S x) : Set α)) 1 x)) • f x
⊢ HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' ⋯ S, f a) =
    ∑ x ∈ s.biUnion S,
      (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) • f x

Tactic:
simp only [prod_const_one, prod_indicator_apply]

Premises used: prod_indicator_apply, Finset.prod_const_one
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
i : ι
hi : i ∈ t
pos :
  Eq.{u_3 + 1} (α := G) (∑ x ∈ t.inf' ⋯ S, HPow.hPow (α := ℤ) (-1) #t • f x)
    (∑ x ∈ s.biUnion S with ∀ (i : ι) (i_1 : i ∈ t), x ∈ S i, HPow.hPow (α := ℤ) (-1) #t • f x)
⊢ HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' ⋯ S, f a) =
    ∑ x ∈ s.biUnion S,
      (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) 1 (Set.indicator (⋂ x ∈ t, (↑(S x) : Set α)) 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]

Premises used: Set.indicator, Pi.one_apply, mul_ite, Set.mem_iInter, Finset.sum_const_zero, MulZeroClass.mul_zero, zero_smul, Finset.smul_sum, ite_smul, mul_one, add_zero, Classical.not_forall, Finset.mem_coe, Finset.sum_ite
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
i : ι
hi : i ∈ t
pos : t.inf' ⋯ S = {x ∈ s.biUnion S | ∀ (i : ι) (i_1 : i ∈ t), x ∈ S i}
⊢ Eq.{u_3 + 1} (α := G) (∑ x ∈ t.inf' ⋯ S, HPow.hPow (α := ℤ) (-1) #t • f x)
    (∑ x ∈ s.biUnion S with ∀ (i : ι) (i_1 : i ∈ t), x ∈ S i, HPow.hPow (α := ℤ) (-1) #t • f x)

Tactic:
congr
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ t.inf' ⋯ S = {x ∈ s.biUnion S | ∀ (i : ι) (i_1 : i ∈ t), x ∈ S i}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
ht : ¬t.Nonempty
neg :
  ∅ ∈ s.powerset →
    ∀ (ht : ¬Finset.Nonempty.{u_1} (α := ι) ∅),
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (card.{u_1} (α := ι) ∅)) (∑ a ∈ s.biUnion S, f a) =
        ∑ x ∈ s.biUnion S,
          (HPow.hPow (α := ℤ) (-1) (card.{u_1} (α := ι) ∅) *
              HMul.hMul (α := ℤ) (∏ i ∈ s \ ∅, 1) (∏ i ∈ ∅, (↑(S i) : Set α).indicator 1 x)) •
            f x
⊢ HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ s.biUnion S, f a) =
    ∑ x ∈ s.biUnion S,
      (HPow.hPow (α := ℤ) (-1) #t * HMul.hMul (α := ℤ) (∏ i ∈ s \ t, 1) (∏ i ∈ t, (↑(S i) : Set α).indicator 1 x)) • f x

Tactic:
obtain rfl := not_nonempty_iff_eq_empty.1 ht

Premises used: Finset.not_nonempty_iff_eq_empty, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
h : ∅ ∈ s.powerset
ht : ¬Finset.Nonempty.{u_1} (α := ι) ∅
⊢ HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) (card.{u_1} (α := ι) ∅)) (∑ a ∈ s.biUnion S, f a) =
    ∑ x ∈ s.biUnion S,
      (HPow.hPow (α := ℤ) (-1) (card.{u_1} (α := ι) ∅) *
          HMul.hMul (α := ℤ) (∏ i ∈ s \ ∅, 1) (∏ i ∈ ∅, (↑(S i) : Set α).indicator 1 x)) •
        f x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
a : ∀ t ∈ s.biUnion S, ∀ x ∈ s, Eq (α := ℤ) 1 ((↑(s.biUnion S) : Set α).indicator 1 t)
⊢ 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:
congr! with t
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : α
h : t ∈ s.biUnion S
x : ι
h_1 : x ∈ s
a : Eq (α := ℤ) 1 (1 t)
a₁ a₂ : Eq (α := ℤ) 1 1
⊢ Eq (α := ℤ) 1 ((↑(s.biUnion S) : Set α).indicator 1 t)

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

Premises used: Pi.one_apply, Set.indicator_of_mem
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
inl :
  Eq.{u_3 + 1} (α := G)
    (∑ a ∈ Finset.biUnion ∅ S,
      HSMul.hSMul (α := ℤ)
        (∏ i ∈ ∅, HSub.hSub (α := ℤ) ((↑(Finset.biUnion ∅ S) : Set α).indicator 1 a) ((↑(S i) : Set α).indicator 1 a))
        (f a))
    0
inr :
  ∀ (hs : s.Nonempty),
    Eq.{u_3 + 1} (α := G)
      (∑ 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))
      0
⊢ Eq.{u_3 + 1} (α := G)
    (∑ 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))
    0

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
S : ι → Finset α
f : α → G
⊢ Eq.{u_3 + 1} (α := G)
    (∑ a ∈ Finset.biUnion ∅ S,
      HSMul.hSMul (α := ℤ)
        (∏ i ∈ ∅, HSub.hSub (α := ℤ) ((↑(Finset.biUnion ∅ S) : Set α).indicator 1 a) ((↑(S i) : Set α).indicator 1 a))
        (f a))
    0

Tactic:
simp [-coe_biUnion, prod_indicator_biUnion_finset_sub_indicator, *]

Premises used: Finset.coe_biUnion, Finset.prod_indicator_biUnion_finset_sub_indicator
-- Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
hs : s.Nonempty
⊢ Eq.{u_3 + 1} (α := G)
    (∑ 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))
    0

Tactic:
simp [-coe_biUnion, prod_indicator_biUnion_finset_sub_indicator, *]

Premises used: Finset.coe_biUnion, Finset.prod_indicator_biUnion_finset_sub_indicator