no goals
α : Type u_1
β : Type ?u.519986
γ : Type ?u.519989
inst✝¹ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
x : α
⊢ x ∈ Finset.biUnion s singleton ↔ x ∈ s
simp only [mem_biUnion, mem_singleton, exists_prop, exists_eq_right']