awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)
have rw : HAdd.hAdd (α := G)
    (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑t : Finset ι)) (∑ a ∈ (↑t : Finset ι).inf' sorry 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: rw [← sum_attach (filter ..)]
-- 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)
    (∑ 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))
have 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)
Tactic: simp only [Int.reduceNeg, prod_sub, sum_comm (s := s.biUnion S), sum_smul, mul_assoc]
-- 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)
    (∑ 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)
have 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
Tactic: congr! 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
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : 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
have 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
Tactic: split_ifs with 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
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
⊢ 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
have 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
Tactic: split_ifs with 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
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
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
have pos : ∀ (i : ι) (hi : i ∈ t),
  HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' sorry 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
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
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
h : t ∈ s.powerset
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
have pos : HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf' sorry 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 [prod_const_one, prod_indicator_apply]
-- 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
t : Finset ι
h : t ∈ s.powerset
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 (α := ℤ) 1 (Set.indicator (⋂ x ∈ t, (↑(S x) : Set α)) 1 x)) • f x
have pos : Eq.{u_3 + 1} (α := G) (∑ x ∈ t.inf' sorry 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: 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]
-- 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
t : Finset ι
h : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ 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)
have pos : t.inf' sorry S = {x ∈ s.biUnion S | ∀ (i : ι) (i_1 : i ∈ t), x ∈ S i}
Tactic: congr
-- 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
t : Finset ι
h : t ∈ s.powerset
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
have 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
Tactic: obtain rfl := not_nonempty_iff_eq_empty.1 ht
Cleared hypotheses: t, h, 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
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ 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))
have a : ∀ t ∈ s.biUnion S, ∀ x ∈ s, Eq (α := ℤ) 1 ((↑(s.biUnion S) : Set α).indicator 1 t)
Tactic: congr! 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
inst_1 : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : α
h : t ∈ s.biUnion S
x : ι
h_1 : x ∈ s
⊢ Eq (α := ℤ) 1 ((↑(s.biUnion S) : Set α).indicator 1 t)
have a : Eq (α := ℤ) 1 (1 t)
Tactic: rw [Set.indicator_of_mem ‹_›, Pi.one_apply]
-- 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
t : α
h : t ∈ s.biUnion S
x : ι
h_1 : x ∈ s
a : Eq (α := ℤ) 1 (1 t)
⊢ Eq (α := ℤ) 1 ((↑(s.biUnion S) : Set α).indicator 1 t)
have a₁ : Eq (α := ℤ) 1 1
Tactic: rw [Set.indicator_of_mem ‹_›, Pi.one_apply]
-- 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,
      HSMul.hSMul (α := ℤ)
        (∏ i ∈ s, HSub.hSub (α := ℤ) ((↑(s.biUnion S) : Set α).indicator 1 a) ((↑(S i) : Set α).indicator 1 a)) (f a))
    0
have 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
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- 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
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
⊢ 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
have 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
Tactic: obtain rfl | hs := s.eq_empty_or_nonempty
-- 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
⊢ 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 : 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)) =
  HAdd.hAdd (α := G)
    (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑t : Finset ι)) (∑ a ∈ (↑t : Finset ι).inf' sorry S, f a))
    (∑ t ∈ s.powerset with ¬t.Nonempty, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ s.biUnion S, 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, *]
-- 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))
⊢ 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₁ : HAdd.hAdd (α := G)
    (∑ t : ↥({x ∈ s.powerset | x.Nonempty}),
      HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #(↑t : Finset ι)) (∑ a ∈ (↑t : Finset ι).inf' sorry 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: 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, *]
-- 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: classical
  rw [← sub_eq_zero]
  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, *]
-- 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 α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
have rw : ∑ a ∈ (s.sup S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
Tactic: rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
-- 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 α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
rw : ∑ a ∈ (s.sup S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
⊢ ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
have rw₁ : ∑ a ∈ (s.biUnion S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
Tactic: rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
-- 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 α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
rw : ∑ a ∈ (s.sup S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
rw₁ : ∑ a ∈ (s.biUnion S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
⊢ ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
have rw₂ : HAdd.hAdd (α := G) (∑ a ∈ (s.biUnion S)ᶜ, f a) (∑ a ∈ s.biUnion S, f a) = ∑ a : α, f a
Tactic: rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
-- 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 α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
rw : ∑ a ∈ (s.sup S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
rw₁ : ∑ a ∈ (s.biUnion S)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
rw₂ : HAdd.hAdd (α := G) (∑ a ∈ (s.biUnion S)ᶜ, f a) (∑ a ∈ s.biUnion S, f a) = ∑ a : α, f a
⊢ ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
have rw₃ : Eq.{u_3 + 1} (α := G) (∑ i : α, f i) (∑ a : α, f a)
Tactic: rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
-- 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 α
inst_2 : Fintype α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ Eq.{u_3 + 1} (α := G) (∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a)
    (∑ t ∈ s.powerset, HSMul.hSMul (β := G) (HPow.hPow (α := ℤ) (-1) #t) (∑ a ∈ t.inf S, f a))
have a : ∑ a ∈ s.inf fun (i : ι) ↦ (S i)ᶜ, f a = HSub.hSub (α := G) (∑ a : α, f a) (∑ a ∈ s.biUnion S, f a)
Tactic: calc
    ∑ a ∈ s.inf fun i ↦ (S i)ᶜ, f a
      = ∑ a, f a - ∑ a ∈ s.biUnion S, f a := by
      rw [← Finset.compl_sup, sup_eq_biUnion, eq_sub_iff_add_eq, sum_compl_add_sum]
    _ = ∑ t ∈ s.powerset.filter (¬ ·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a
          + ∑ t ∈ s.powerset.filter (·.Nonempty), (-1) ^ #t • ∑ a ∈ t.inf S, f a := by
      simp [← sum_attach (filter ..), inclusion_exclusion_sum_biUnion, inf'_eq_inf, filter_eq',
        sub_eq_add_neg, pow_succ]
    _ = ∑ t ∈ s.powerset, (-1) ^ #t • ∑ a ∈ t.inf S, f a := sum_filter_not_add_sum_filter ..