case h
α : Type u_1
β : Type u_2
γ : Type ?u.230579
ι : Sort u_3
ι' : Sort ?u.230585
ι₂ : Sort ?u.230588
κ : ι → Sort ?u.230593
κ₁ : ι → Sort ?u.230598
κ₂ : ι → Sort ?u.230603
κ' : ι' → Sort ?u.230608
s : ι → Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (⋃ (i : ι), s i) ×ˢ t ↔ x✝ ∈ ⋃ (i : ι), s i ×ˢ t
α : Type u_1
β : Type u_2
γ : Type ?u.230579
ι : Sort u_3
ι' : Sort ?u.230585
ι₂ : Sort ?u.230588
κ : ι → Sort ?u.230593
κ₁ : ι → Sort ?u.230598
κ₂ : ι → Sort ?u.230603
κ' : ι' → Sort ?u.230608
s : ι → Set α
t : Set β
⊢ (⋃ (i : ι), s i) ×ˢ t = ⋃ (i : ι), s i ×ˢ t
ext
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.230579
ι : Sort u_3
ι' : Sort ?u.230585
ι₂ : Sort ?u.230588
κ : ι → Sort ?u.230593
κ₁ : ι → Sort ?u.230598
κ₂ : ι → Sort ?u.230603
κ' : ι' → Sort ?u.230608
s : ι → Set α
t : Set β
x✝ : α × β
⊢ x✝ ∈ (⋃ (i : ι), s i) ×ˢ t ↔ x✝ ∈ ⋃ (i : ι), s i ×ˢ t
simp