α : Type u_1
β : Type u_2
γ : Type ?u.17061
δ : Type ?u.17064
ι : Sort ?u.17067
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot f
⊢ map (Prod.snd ∘ fun p => (p.snd, p.fst)) (g ×ˢ f) = g
α : Type u_1
β : Type u_2
γ : Type ?u.17061
δ : Type ?u.17064
ι : Sort ?u.17067
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot f
⊢ map Prod.snd (f ×ˢ g) = g
rw [prod_comm, map_map]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.17061
δ : Type ?u.17064
ι : Sort ?u.17067
s : Set α
t : Set β
f✝ : Filter α
g✝ : Filter β
f : Filter α
g : Filter β
inst✝ : NeBot f
⊢ map (Prod.snd ∘ fun p => (p.snd, p.fst)) (g ×ˢ f) = g
apply map_fst_prod