case h
α✝ : Type ?u.233741
β✝ : Type ?u.233744
γ : Type ?u.233747
ι✝ : Sort ?u.233750
ι'✝ : Sort ?u.233753
ι₂ : Sort ?u.233756
κ : ι✝ → Sort ?u.233761
κ₁ : ι✝ → Sort ?u.233766
κ₂ : ι✝ → Sort ?u.233771
κ' : ι'✝ → Sort ?u.233776
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
s : ι → Set α
t : ι' → Set β
x✝ : α × β
⊢ (x✝ ∈ ⋃ (x : ι × ι'), s x.fst ×ˢ t x.snd) ↔ x✝ ∈ (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i
α✝ : Type ?u.233741
β✝ : Type ?u.233744
γ : Type ?u.233747
ι✝ : Sort ?u.233750
ι'✝ : Sort ?u.233753
ι₂ : Sort ?u.233756
κ : ι✝ → Sort ?u.233761
κ₁ : ι✝ → Sort ?u.233766
κ₂ : ι✝ → Sort ?u.233771
κ' : ι'✝ → Sort ?u.233776
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
s : ι → Set α
t : ι' → Set β
⊢ (⋃ (x : ι × ι'), s x.fst ×ˢ t x.snd) = (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i
ext
no goals
case h
α✝ : Type ?u.233741
β✝ : Type ?u.233744
γ : Type ?u.233747
ι✝ : Sort ?u.233750
ι'✝ : Sort ?u.233753
ι₂ : Sort ?u.233756
κ : ι✝ → Sort ?u.233761
κ₁ : ι✝ → Sort ?u.233766
κ₂ : ι✝ → Sort ?u.233771
κ' : ι'✝ → Sort ?u.233776
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
s : ι → Set α
t : ι' → Set β
x✝ : α × β
⊢ (x✝ ∈ ⋃ (x : ι × ι'), s x.fst ×ˢ t x.snd) ↔ x✝ ∈ (⋃ (i : ι), s i) ×ˢ ⋃ (i : ι'), t i
simp