case a
α : Type u_1
β : Type u_2
γ : Type ?u.16299
δ : Type ?u.16302
ι : Sort ?u.16305
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot g
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
α : Type u_1
β : Type u_2
γ : Type ?u.16299
δ : Type ?u.16302
ι : Sort ?u.16305
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot g
⊢ map Prod.fst (f ×ˢ g) = f
ext s
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.16299
δ : Type ?u.16302
ι : Sort ?u.16305
s✝ : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot g
s : Set α
⊢ s ∈ map Prod.fst (f ×ˢ g) ↔ s ∈ f
simp only [mem_map, mem_prod_iff_left, mem_preimage, eventually_const, ← subset_def,
  exists_mem_subset_iff]