no goals
α : Type u_2
α' : Type ?u.45119
β : Type u_1
β' : Type ?u.45125
γ : Type ?u.45128
γ' : Type ?u.45131
δ : Type ?u.45134
δ' : Type ?u.45137
ε : Type ?u.45140
ε' : Type ?u.45143
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 : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
⊢ map₂ f (pure a) l = l
rw [map₂_pure_left, show f a = id from funext h, map_id]