no goals
α : Type u_2
α' : Type ?u.28301
β : Type u_3
β' : Type ?u.28307
γ : Type u_1
γ' : Type ?u.28313
δ : Type ?u.28316
δ' : Type ?u.28319
ε : Type ?u.28322
ε' : Type ?u.28325
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 : γ
u : Set γ
h : u ∈ map (fun a => m a b) f
⊢ image2 m ((fun a => m a b) ⁻¹' u) {b} ⊆ u
rw [image2_singleton_right, image_subset_iff]