no goals
α : Type u_1
β : Type ?u.139917
γ : Type ?u.139920
inst✝ : DecidableEq α
s✝ s₁ s₂ t✝ t₁ t₂ u v : Finset α
a✝ b : α
s t : Finset α
h : _root_.Disjoint s t
a : α
⊢ a ∈ disjUnion s t h ↔ a ∈ s ∪ t
simp