no goals
α : Type u_2
β : Type u_1
γ : Type ?u.498743
inst✝ : DecidableEq β
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
⊢ ↑(Finset.biUnion s t) = ⋃ (x : α) (_ : x ∈ ↑s), ↑(t x)
simp [Set.ext_iff, mem_biUnion, Set.mem_iUnion, iff_self_iff, mem_coe, imp_true_iff]