α : Type u_2
β : Type u_1
γ : Type ?u.14817
δ : Type ?u.14820
ι : Sort ?u.14823
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ Prod.swap <$> (g ×ˢ f) = map (fun p => (p.snd, p.fst)) (g ×ˢ f)
α : Type u_2
β : Type u_1
γ : Type ?u.14817
δ : Type ?u.14820
ι : Sort ?u.14823
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ f ×ˢ g = map (fun p => (p.snd, p.fst)) (g ×ˢ f)
rw [prod_comm', ← map_swap_eq_comap_swap]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.14817
δ : Type ?u.14820
ι : Sort ?u.14823
s : Set α
t : Set β
f : Filter α
g : Filter β
⊢ Prod.swap <$> (g ×ˢ f) = map (fun p => (p.snd, p.fst)) (g ×ˢ f)
rfl