no goals
ι : Type ?u.311298
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset γ
t : γ → Finset α
hs : Set.PairwiseDisjoint (↑s) t
⊢ ∏ x in Finset.biUnion s t, f x = ∏ x in s, ∏ i in t x, f i
rw [← disjiUnion_eq_biUnion _ _ hs, prod_disjiUnion]