-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
theorem prod_add (f g : ι → α) (s : Finset ι) :
    ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (f i + g i) = ∏ i ∈ s, ∑ p ∈ {True, False}, if p then f i else g i

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i

Tactic:
classical
calc
  ∏ i ∈ s, (f i + g i) =
      ∏ i ∈ s, ∑ p ∈ ({True, False} : Finset Prop), if p then f i else g i := by simp
  _ = ∑ p ∈ (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
        ∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 := prod_sum _ _ _
  _ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
    sum_bij'
      (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h})
      (fun t _ a _ => a ∈ t)
      (by simp)
      (by simp [Classical.em])
      (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
      (by simp_rw [Finset.ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
      (fun a _ ↦ by
        simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
          Subtype.map_coe, id_eq, prod_attach, filter_congr_decidable]
        congr 2 with x
        simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
        tauto)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ (a : Finset ι) (ha : a ∈ s.powerset), (fun t x a x => a ∈ t) a ha ∈ s.pi fun x => {True, False}

Tactic:
simp [Classical.em]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x => {True, False}
⊢ (∏ a_1 ∈ s.attach, if a ↑a_1 ⋯ then f ↑a_1 else g ↑a_1) =
    (∏ a ∈ (fun f x => filter (fun a => ∃ (h : a ∈ s), f a h) s) a x✝, f a) *
      ∏ a ∈ s \ (fun f x => filter (fun a => ∃ (h : a ∈ s), f a h) s) a x✝, g a

Tactic:
simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
  Subtype.map_coe, id_eq, prod_attach, filter_congr_decidable]

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x => {True, False}
⊢ (∏ x ∈ filter (fun x => ∃ (h : x ∈ s), a x ⋯) s, f x) * ∏ x ∈ filter (fun x => ∃ (h : x ∈ s), ¬a x ⋯) s, g x =
    (∏ x ∈ filter (fun a_1 => ∃ (h : a_1 ∈ s), a a_1 h) s, f x) *
      ∏ x ∈ s \ filter (fun a_1 => ∃ (h : a_1 ∈ s), a a_1 h) s, g x

Proof state:
case e_a.e_s.h
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x => {True, False}
x : ι
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)

Tactic:
tauto

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ (a : Finset ι) (ha : a ∈ s.powerset),
    (fun f x => filter (fun a => ∃ (h : a ∈ s), f a h) s) ((fun t x a x => a ∈ t) a ha) ⋯ = a

Tactic:
simp_rw [Finset.ext_iff, @mem_filter _ _ (id _), mem_powerset]

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ a ⊆ s, ∀ (a_1 : ι), (a_1 ∈ s ∧ ∃ (_ : a_1 ∈ s), a_1 ∈ a) ↔ a_1 ∈ a

Tactic:
tauto

Result:
no goals

Proof state:
case e_a.e_s.h
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x => {True, False}
x : ι
⊢ x ∈ filter (fun x => ∃ (h : x ∈ s), ¬a x ⋯) s ↔ x ∈ s \ filter (fun a_1 => ∃ (h : a_1 ∈ s), a a_1 h) s

Tactic:
simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]

Result:
case e_a.e_s.h
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x => {True, False}
x : ι
⊢ x ∈ s → ((∃ (h : x ∈ s), ¬a x ⋯) ↔ x ∈ s → ∀ (x_1 : x ∈ s), ¬a x x_1)

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop) (ha : a ∈ s.pi fun x => {True, False}),
    (fun f x => filter (fun a => ∃ (h : a ∈ s), f a h) s) a ha ∈ s.powerset

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (f i + g i) = ∑ t ∈ s.powerset, (∏ i ∈ t, f i) * ∏ i ∈ s \ t, g i

Tactic:
calc
  ∏ i ∈ s, (f i + g i) =
      ∏ i ∈ s, ∑ p ∈ ({True, False} : Finset Prop), if p then f i else g i := by simp
  _ = ∑ p ∈ (s.pi fun _ => {True, False} : Finset (∀ a ∈ s, Prop)),
        ∏ a ∈ s.attach, if p a.1 a.2 then f a.1 else g a.1 := prod_sum _ _ _
  _ = ∑ t ∈ s.powerset, (∏ a ∈ t, f a) * ∏ a ∈ s \ t, g a :=
    sum_bij'
      (fun f _ ↦ {a ∈ s | ∃ h : a ∈ s, f a h})
      (fun t _ a _ => a ∈ t)
      (by simp)
      (by simp [Classical.em])
      (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto)
      (by simp_rw [Finset.ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto)
      (fun a _ ↦ by
        simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk,
          Subtype.map_coe, id_eq, prod_attach, filter_congr_decidable]
        congr 2 with x
        simp only [mem_filter, mem_sdiff, not_and, not_exists, and_congr_right_iff]
        tauto)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x => {True, False}
⊢ (∏ x ∈ filter (fun x => ∃ (h : x ∈ s), a x ⋯) s, f x) * ∏ x ∈ filter (fun x => ∃ (h : x ∈ s), ¬a x ⋯) s, g x =
    (∏ x ∈ filter (fun a_1 => ∃ (h : a_1 ∈ s), a a_1 h) s, f x) *
      ∏ x ∈ s \ filter (fun a_1 => ∃ (h : a_1 ∈ s), a a_1 h) s, g x

Tactic:
congr 2 with x

Result:
case e_a.e_s.h
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
a : (a : ι) → a ∈ s → Prop
x✝ : a ∈ s.pi fun x => {True, False}
x : ι
⊢ x ∈ filter (fun x => ∃ (h : x ∈ s), ¬a x ⋯) s ↔ x ∈ s \ filter (fun a_1 => ∃ (h : a_1 ∈ s), a a_1 h) s

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ a a_1 h ∈ {False}) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1

Tactic:
tauto

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop) (ha : a ∈ s.pi fun x => {True, False}),
    (fun t x a x => a ∈ t) ((fun f x => filter (fun a => ∃ (h : a ∈ s), f a h) s) a ha) ⋯ = a

Tactic:
simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommSemiring α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∀ (a : (a : ι) → a ∈ s → Prop),
    (∀ (a_1 : ι) (h : a_1 ∈ s), a a_1 h = True ∨ a a_1 h ∈ {False}) →
      ∀ (x : ι) (x_1 : x ∈ s), (x ∈ s ∧ ∃ (h : x ∈ s), a x h) ↔ a x x_1