no goals
α : Type u_1
β : Type u_2
γ : Type ?u.8812
ι : Sort ?u.8815
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
hg : Monotone g
⊢ ⋂₀ {s | s ∈ Filter.lift f g} = ⋂ (s : Set α) (_ : s ∈ f), ⋂₀ {t | t ∈ g s}
simp only [sInter_eq_biInter, mem_setOf_eq, Filter.mem_sets, mem_lift_sets hg, iInter_exists,
  iInter_and, @iInter_comm _ (Set β)]