case h
α : Type u_1
β : Type ?u.281523
γ : Type ?u.281526
ι : Sort ?u.281529
ι' : Sort ?u.281532
ι₂ : Sort ?u.281535
κ : ι → Sort ?u.281540
κ₁ : ι → Sort ?u.281545
κ₂ : ι → Sort ?u.281550
κ' : ι' → Sort ?u.281555
π : α → Type u_2
i : Set α
s : (a : α) → Set (π a)
x✝ : (i : α) → π i
⊢ x✝ ∈ pi i s ↔ x✝ ∈ ⋂ (a : α) (_ : a ∈ i), eval a ⁻¹' s a
α : Type u_1
β : Type ?u.281523
γ : Type ?u.281526
ι : Sort ?u.281529
ι' : Sort ?u.281532
ι₂ : Sort ?u.281535
κ : ι → Sort ?u.281540
κ₁ : ι → Sort ?u.281545
κ₂ : ι → Sort ?u.281550
κ' : ι' → Sort ?u.281555
π : α → Type u_2
i : Set α
s : (a : α) → Set (π a)
⊢ pi i s = ⋂ (a : α) (_ : a ∈ i), eval a ⁻¹' s a
ext
no goals
case h
α : Type u_1
β : Type ?u.281523
γ : Type ?u.281526
ι : Sort ?u.281529
ι' : Sort ?u.281532
ι₂ : Sort ?u.281535
κ : ι → Sort ?u.281540
κ₁ : ι → Sort ?u.281545
κ₂ : ι → Sort ?u.281550
κ' : ι' → Sort ?u.281555
π : α → Type u_2
i : Set α
s : (a : α) → Set (π a)
x✝ : (i : α) → π i
⊢ x✝ ∈ pi i s ↔ x✝ ∈ ⋂ (a : α) (_ : a ∈ i), eval a ⁻¹' s a
simp