α : Type u_1
β : Type u_2
γ : Type ?u.44252
δ : Type ?u.44255
ι : Sort ?u.44258
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
b : β
⊢ map ((fun g => g b) ∘ Prod.mk) f = map (fun a => (a, b)) f
α : Type u_1
β : Type u_2
γ : Type ?u.44252
δ : Type ?u.44255
ι : Sort ?u.44258
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
b : β
⊢ f ×ˢ pure b = map (fun a => (a, b)) f
rw [prod_eq, seq_pure, map_map]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44252
δ : Type ?u.44255
ι : Sort ?u.44258
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : Filter α
b : β
⊢ map ((fun g => g b) ∘ Prod.mk) f = map (fun a => (a, b)) f
rfl