no goals
ι : Type ?u.309859
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝ : CommMonoid β
s : Finset α
t : Finset γ
f : α → β
g : γ → β
⊢ ∏ x in disjSum s t, Sum.elim f g x = (∏ x in s, f x) * ∏ x in t, g x
simp