no goals
α : Type u_1
β : Type ?u.71521
γ : Type ?u.71524
ι : Sort u_2
κ : ι → Sort ?u.71532
inst✝ : LE α
S : Set (LowerSet α)
s t : LowerSet α
a : α
f : ι → LowerSet α
⊢ ↑(⨅ (i : ι), f i) = ⋂ (i : ι), ↑(f i)
simp_rw [iInf, coe_sInf, mem_range, iInter_exists, iInter_iInter_eq']