no goals
ι : Type ?u.306898
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
h : s₁ ⊆ s₂
⊢ (∏ x in s₂ \ s₁, f x) * ∏ x in s₁, f x = ∏ x in s₂, f x
rw [← prod_union sdiff_disjoint, sdiff_union_of_subset h]