no goals
α : Type u_2
β : Type u_1
γ : Type ?u.498019
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
b : β
⊢ b ∈ Finset.biUnion s t ↔ ∃ a, a ∈ s ∧ b ∈ t a
simp only [mem_def, biUnion_val, mem_dedup, mem_bind, exists_prop]