member of finite union is in one of the sets

Stream: mathlib4

[Yifan Bai]

How to prove the following lemma?

lemma h (t : Finset E) (O : E → Set E) : ∀ u ∈ (⋃ x ∈ t, O x), ∃ x ∈ t, u ∈ O x := by sorry

which is simply to prove the member of finite union is in one of the sets. I didn't find any given lemma in mathlib...

[Daniel Weber]

You can use docs#Set.mem_iUnion, or let simp apply it for you:

import Mathlib

lemma h (t : Finset E) (O : E → Set E) : ∀ u ∈ (⋃ x ∈ t, O x), ∃ x ∈ t, u ∈ O x := by
  intro u hu
  simpa using hu

[Yifan Bai]

Daniel Weber said:

You can use docs#Set.mem_iUnion, or let simp apply it for you:

import Mathlib

lemma h (t : Finset E) (O : E → Set E) : ∀ u ∈ (⋃ x ∈ t, O x), ∃ x ∈ t, u ∈ O x := by
  intro u hu
  simpa using hu

Thank you! Sorry for this easy problem, I'm really new at this... :sob: