case h
ι : Type u_2
α : Type u_1
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ (x ∈ ⋃ (i : ι), s i) ↔ x ∈ univ
ι : Type u_2
α : Type u_1
s : ι → Set α
hs : IndexedPartition s
⊢ (⋃ (i : ι), s i) = univ
ext x
no goals
case h
ι : Type u_2
α : Type u_1
s : ι → Set α
hs : IndexedPartition s
x : α
⊢ (x ∈ ⋃ (i : ι), s i) ↔ x ∈ univ
simp [hs.exists_mem x]