no goals
α : Type u_3
α' : Type u_5
β : Type u_4
β' : Type u_6
γ : Type u_2
γ' : Type ?u.39560
δ : Type u_1
δ' : Type ?u.39566
ε : Type ?u.39569
ε' : Type ?u.39572
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 : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)
simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]