α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.43964
ι : Sort ?u.43967
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.43964
ι : Sort ?u.43967
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B
rw [Filter.pure_prod]
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.43964
ι : Sort ?u.43967
s : Set α
t : Set β
f✝ : Filter α
g : Filter β
f : α → β → γ
a : α
B : Filter β
⊢ map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
rfl