no goals
α : Type u_2
β : Type ?u.286650
γ : Type ?u.286653
ι : Sort ?u.286656
ι' : Sort ?u.286659
ι₂ : Sort ?u.286662
κ : ι → Sort ?u.286667
κ₁ : ι → Sort ?u.286672
κ₂ : ι → Sort ?u.286677
κ' : ι' → Sort ?u.286682
π : α → Type u_1
t : (i : α) → Set (π i)
⊢ pi univ t = ⋂ (i : α), eval i ⁻¹' t i
simp only [pi_def, iInter_true, mem_univ]