no goals
α : Type u_1
β : Type u_2
γ : Type ?u.8191
ι : Sort ?u.8194
f f₁ f₂ : Filter α
g g₁ g₂ : Set α → Filter β
hg : Monotone g
s : Set β
⊢ (∃ i, i ∈ f ∧ ∃ x, x ∈ g i ∧ id x ⊆ s) ↔ ∃ t, t ∈ f ∧ s ∈ g t
simp only [id, exists_mem_subset_iff]