no goals
α : Type u_2
β : Type u_3
γ : Type u_1
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ Finset.biUnion (s ×ˢ t) f = Finset.biUnion s fun a => Finset.biUnion t fun b => f (a, b)
classical simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]
no goals
α : Type u_2
β : Type u_3
γ : Type u_1
s✝ s' : Finset α
t✝ t' : Finset β
a : α
b : β
inst✝ : DecidableEq γ
s : Finset α
t : Finset β
f : α × β → Finset γ
⊢ Finset.biUnion (s ×ˢ t) f = Finset.biUnion s fun a => Finset.biUnion t fun b => f (a, b)
simp_rw [product_eq_biUnion, biUnion_biUnion, image_biUnion]