no goals
α : Type u_2
β : Type u_1
γ : Type ?u.483883
s s₁ s₂ : Finset α
t t₁ t₂ : α → Finset β
b : β
h : Set.PairwiseDisjoint (↑s) t
⊢ b ∈ disjiUnion s t h ↔ ∃ a, a ∈ s ∧ b ∈ t a
simp only [mem_def, disjiUnion_val, mem_bind, exists_prop]