have ⟨_, h, _⟩ := List.mem_fold_union_iff.mp h
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h : e ∈ List.foldr Union.union ∅ (List.map f l)
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x
case mp.mk
β : Type u_2
inst✝ : DecidableEq β
α : Type u_1
e : β
s : Finset α
f : α → Finset β
l : List α
nodup✝ : Multiset.Nodup (Quot.mk Setoid.r l)
h✝ : e ∈ List.foldr Union.union ∅ (List.map f l)
w✝ : Finset β
h : w✝ ∈ List.map f l
right✝ : e ∈ w✝
⊢ ∃ x ∈ { val := Quot.mk Setoid.r l, nodup := nodup✝ }, e ∈ f x