no goals
α : Type u_2
α' : Type ?u.36798
β : Type u_4
β' : Type ?u.36804
γ : Type u_3
γ' : Type ?u.36810
δ : Type u_1
δ' : Type ?u.36816
ε : Type ?u.36819
ε' : Type ?u.36822
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 : γ
m : α → γ → δ
n : β → γ
⊢ map₂ m f (map n g) = map₂ (fun a b => m a (n b)) f g
rw [map₂_swap, map₂_map_left, map₂_swap]