ext a
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
⊢ Finset.subtype p (s1 ∪ s2) = Finset.subtype p s1 ∪ Finset.subtype p s2
case a
α : Type u_1
p : α → Prop
inst✝¹ : DecidableEq α
inst✝ : DecidablePred p
s1 s2 : Finset α
a : Subtype p
⊢ a ∈ Finset.subtype p (s1 ∪ s2) ↔ a ∈ Finset.subtype p s1 ∪ Finset.subtype p s2