no goals
ι : Type ?u.312096
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g : α → β
inst✝ : CommMonoid β
σ : α → Type u_1
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x in Finset.sigma s t, f x = ∏ a in s, ∏ s in t a, f { fst := a, snd := s }
simp_rw [← disjiUnion_map_sigma_mk, prod_disjiUnion, prod_map, Function.Embedding.sigmaMk_apply]