no goals
α : Type u_2
α' : Type ?u.38335
β : Type u_3
β' : Type ?u.38341
γ : Type u_1
γ' : Type ?u.38347
δ : Type ?u.38350
δ' : Type ?u.38353
ε : Type ?u.38356
ε' : Type ?u.38359
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 : γ
n : β → α → γ
h_comm : ∀ (a : α) (b : β), m a b = n b a
⊢ map₂ (fun a b => m b a) g f = map₂ n g f
simp_rw [h_comm]