ι : Type ?u.288824
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
f : α → β
this : DecidableEq α
⊢ (∏ x in filter p s, f x) * ∏ x in filter (fun x => ¬p x) s, f x = ∏ x in s, f x
ι : Type ?u.288824
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
f : α → β
⊢ (∏ x in filter p s, f x) * ∏ x in filter (fun x => ¬p x) s, f x = ∏ x in s, f x
have := Classical.decEq α
no goals
ι : Type ?u.288824
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝² : CommMonoid β
s : Finset α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : α) → Decidable ¬p x
f : α → β
this : DecidableEq α
⊢ (∏ x in filter p s, f x) * ∏ x in filter (fun x => ¬p x) s, f x = ∏ x in s, f x
rw [← prod_union (disjoint_filter_filter_neg s s p), filter_union_filter_neg_eq]