no goals
ι : Type ?u.319435
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
s : Finset α
t : Finset γ
g : α → γ
h : ∀ (x : α), x ∈ s → g x ∈ t
f : α → β
⊢ ∏ y in t, ∏ x in filter (fun x => g x = y) s, f x = ∏ x in s, f x
rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]