-- Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
lemma prod_indicator_biUnion_sub_indicator (hs : s.Nonempty) (S : ι → Finset α) (a : α) :
    ∏ i ∈ s, (Set.indicator (s.biUnion S) 1 a - Set.indicator (S i) 1 a) = (0 : ℤ)

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
by_cases ha : a ∈ s.biUnion S

Result:
case pos
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
ha : a ∈ s.biUnion S
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

case neg
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
ha : a ∉ s.biUnion S
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
ha✝ : a ∈ s.biUnion S
i : ι
hi : i ∈ s
ha : a ∈ S i
⊢ (↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a = 0

Tactic:
simp [*, -coe_biUnion]

Result:
no goals

Proof state:
case neg
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
ha : a ∉ s.biUnion S
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
obtain ⟨i, hi⟩ := hs

Result:
case neg.intro
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
a : α
ha : a ∉ s.biUnion S
i : ι
hi : i ∈ s
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Proof state:
case pos.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
ha✝ : a ∈ s.biUnion S
i : ι
hi : i ∈ s
ha : a ∈ S i
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
exact prod_eq_zero hi <| by simp [*, -coe_biUnion]

Result:
no goals

Proof state:
case neg.intro
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
a : α
ha✝ : a ∉ s.biUnion S
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
exact prod_eq_zero hi <| by simp [*, -coe_biUnion]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
a : α
ha✝ : a ∉ s.biUnion S
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ (↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a = 0

Tactic:
simp [*, -coe_biUnion]

Result:
no goals

Proof state:
case pos
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
ha : a ∈ s.biUnion S
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
obtain ⟨i, hi, ha⟩ := mem_biUnion.1 ha

Result:
case pos.intro.intro
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
hs : s.Nonempty
S : ι → Finset α
a : α
ha✝ : a ∈ s.biUnion S
i : ι
hi : i ∈ s
ha : a ∈ S i
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Proof state:
case neg.intro
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
a : α
ha : a ∉ s.biUnion S
i : ι
hi : i ∈ s
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

Tactic:
have ha : a ∉ S i := fun h ↦ ha <| subset_biUnion_of_mem _ hi h

Result:
case neg.intro
ι : Type u_1
α : Type u_2
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
a : α
ha✝ : a ∉ s.biUnion S
i : ι
hi : i ∈ s
ha : a ∉ S i
⊢ ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0