no goals
α : Type u_4
α' : Type ?u.37656
β : Type u_5
β' : Type ?u.37662
γ : Type u_1
γ' : Type ?u.37668
δ : Type u_3
δ' : Type ?u.37674
ε : Type u_2
ε' : Type u_6
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 : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)
simp only [map₂_map₂_left, map₂_map₂_right, h_assoc]