awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
ha : Membership.mem (γ := Set α) (⋂ i ∈ t, S i) a
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
have ha₁ : ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i
Tactic: simp only [Set.mem_iInter] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
ha : ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
have neg : ∀ (i : ι) (hi : i ∈ t), Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
Tactic: rcases ht with ⟨i, hi⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ha : ∀ (i : ι) (i_1 : i ∈ t), a ∈ S i
i : ι
hi : i ∈ t
⊢ Membership.mem (γ := Set α) (⋃ i ∈ s, S i) a
have neg : ∃ i ∈ s, a ∈ S i
Tactic: simp only [Set.mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ 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
have pos : 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: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ 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
have rw : Eq.{u_3 + 1} (α := G) (∑ x ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #x • Set.indicator (⋂ i ∈ x, S i) f a)
  (∑ t ∈ s.powerset, HPow.hPow (α := ℤ) (-1) #t • Set.indicator (⋂ i ∈ t, S i) f a)
Tactic: rw [sum_filter_add_sum_filter_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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 ∈ 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)
have simp : 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: simp only [Int.reduceNeg, prod_sub, prod_const_one, mul_one, sum_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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.{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)
have 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
Tactic: congr! 1 with t
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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 * ∏ i ∈ t, (S i).indicator 1 a) • f a
have 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
Tactic: simp only [prod_const_one, prod_indicator_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (hypothesis)
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
⊢ HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((S i).indicator 1 a)) (f a) = 0
have this : 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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((S i).indicator 1 a)) (f a) = 0
have hs : s.Nonempty
Tactic: rw [← this, prod_indicator_biUnion_sub_indicator, zero_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (hypothesis)
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
⊢ s.Nonempty
have ha₁ : ∃ i ∈ s, a ∈ S i
Tactic: simp only [Set.mem_iUnion, exists_prop] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ s.Nonempty
have hs : ∀ (i : ι) (hi : i ∈ s), s.Nonempty
Tactic: rcases ha with ⟨i, hi, -⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ 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
have 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)
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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)
⊢ 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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ 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
have 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)
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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)
⊢ 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
have i₃ : HSMul.hSMul (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) 1 ((S i).indicator 1 a)) (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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
G : Type u_3
inst : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ 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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
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
⊢ 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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.InclusionExclusion (goal)
Goal:
ι : Type u_1
α : Type u_2
s : Finset ι
inst : DecidableEq α
hs : s.Nonempty
S : ι → Finset α
a : α
⊢ Eq (α := ℤ) (∏ i ∈ s, HSub.hSub (α := ℤ) ((↑(s.biUnion S) : Set α).indicator 1 a) ((↑(S i) : Set α).indicator 1 a)) 0
have h : ∀ x ∈ s, (↑(s.biUnion S) : Set α) = ⋃ i ∈ s, (↑(S i) : Set α)
Tactic: convert! prod_indicator_biUnion_sub_indicator hs (fun i ↦ S i) a
-- 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
⊢ 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))
have 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' sorry S, f a)) =
  0
Tactic: rw [← sub_eq_zero]