no goals
α : Type u_1
β : Type u_2
γ : Type ?u.505331
inst✝¹ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
inst✝ : DecidableEq α
a : α
x : β
⊢ x ∈ Finset.biUnion (insert a s) t ↔ x ∈ t a ∪ Finset.biUnion s t
simp only [mem_biUnion, exists_prop, mem_union, mem_insert, or_and_right, exists_or,
  exists_eq_left]