no goals
α : Type u_2
β : Type ?u.476654
γ : Type ?u.476657
ι : Type ?u.476660
M : Type u_3
M' : Type ?u.476666
N : Type u_1
P : Type ?u.476672
G : Type ?u.476675
H : Type ?u.476678
R : Type ?u.476681
S : Type ?u.476684
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ prod (filter p f) g * prod (filter (fun a => ¬p a) f) g = prod f g
classical simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not,
  Finsupp.prod]
no goals
α : Type u_2
β : Type ?u.476654
γ : Type ?u.476657
ι : Type ?u.476660
M : Type u_3
M' : Type ?u.476666
N : Type u_1
P : Type ?u.476672
G : Type ?u.476675
H : Type ?u.476678
R : Type ?u.476681
S : Type ?u.476684
inst✝¹ : Zero M
p : α → Prop
f : α →₀ M
inst✝ : CommMonoid N
g : α → M → N
⊢ prod (filter p f) g * prod (filter (fun a => ¬p a) f) g = prod f g
simp_rw [prod_filter_index, support_filter, Finset.prod_filter_mul_prod_filter_not,
Finsupp.prod]