Problem with existential that seems to take an argument

Stream: new members

[Andrew Lubrino]

In my code below, I have hb : ∃ (t : set U) (H : t ∈ F), x ∈ t and I'm trying to introduce a t : set U to clear the existential so that I can work with this. When I use intro or assume I get an error, and when I use intros, no new assumptions appear. Also, how can I use / work around (H : t ∈ F) in the statement I have?

import data.set
open set

variable {U : Type}
variables F G : set (set U)

theorem sub_of_family_of_family (ha : F ⊆ G) : ⋃₀F ⊆ ⋃₀G :=
begin
  intros x hb,
  rw mem_sUnion at hb,
  sorry
end

[Alex J. Best]

You need to uses some version of tactic#cases to break up an existential in the hypotheses, e.g. rcases hb with \<t, ht, hx\>

[Andrew Lubrino]

Awesome, thank you.