no goals
α : Type u_1
α' : Type ?u.45411
β : Type u_2
β' : Type ?u.45417
γ : Type ?u.45420
γ' : Type ?u.45423
δ : Type ?u.45426
δ' : Type ?u.45429
ε : Type ?u.45432
ε' : Type ?u.45435
m : α → β → γ
f✝ f₁ f₂ : Filter α
g g₁ g₂ : Filter β
h✝ h₁ h₂ : Filter γ
s s₁ s₂ : Set α
t t₁ t₂ : Set β
u : Set γ
v : Set δ
a : α
b✝ : β
c : γ
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
l : Filter α
⊢ map₂ f l (pure b) = l
rw [map₂_pure_right, funext h, map_id']