no goals
α : Type u_2
α' : Type ?u.29150
β : Type u_3
β' : Type ?u.29156
γ : Type u_1
γ' : Type ?u.29162
δ : Type ?u.29165
δ' : Type ?u.29168
ε : Type ?u.29171
ε' : Type ?u.29174
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 : γ
⊢ map₂ m (pure a) (pure b) = pure (m a b)
rw [map₂_pure_right, map_pure]