case h
α : Type u_2
β : Type ?u.288374
γ : Type ?u.288377
ι : Sort u_3
ι' : Sort ?u.288383
ι₂ : Sort ?u.288386
κ : ι → Sort ?u.288391
κ₁ : ι → Sort ?u.288396
κ₂ : ι → Sort ?u.288401
κ' : ι' → Sort ?u.288406
π : α → Type u_1
t : (i : α) → ι → Set (π i)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ (x : α → ι), pi univ fun i => t i (x i)) ↔ x✝ ∈ pi univ fun i => ⋃ (j : ι), t i j
α : Type u_2
β : Type ?u.288374
γ : Type ?u.288377
ι : Sort u_3
ι' : Sort ?u.288383
ι₂ : Sort ?u.288386
κ : ι → Sort ?u.288391
κ₁ : ι → Sort ?u.288396
κ₂ : ι → Sort ?u.288401
κ' : ι' → Sort ?u.288406
π : α → Type u_1
t : (i : α) → ι → Set (π i)
⊢ (⋃ (x : α → ι), pi univ fun i => t i (x i)) = pi univ fun i => ⋃ (j : ι), t i j
ext
no goals
case h
α : Type u_2
β : Type ?u.288374
γ : Type ?u.288377
ι : Sort u_3
ι' : Sort ?u.288383
ι₂ : Sort ?u.288386
κ : ι → Sort ?u.288391
κ₁ : ι → Sort ?u.288396
κ₂ : ι → Sort ?u.288401
κ' : ι' → Sort ?u.288406
π : α → Type u_1
t : (i : α) → ι → Set (π i)
x✝ : (i : α) → π i
⊢ (x✝ ∈ ⋃ (x : α → ι), pi univ fun i => t i (x i)) ↔ x✝ ∈ pi univ fun i => ⋃ (j : ι), t i j
simp [Classical.skolem]