no goals
α : Type u_2
α' : Type ?u.27454
β : Type u_3
β' : Type ?u.27460
γ : Type u_1
γ' : Type ?u.27466
δ : Type ?u.27469
δ' : Type ?u.27472
ε : Type ?u.27475
ε' : Type ?u.27478
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 b => m a b) g
⊢ image2 m {a} ((fun b => m a b) ⁻¹' u) ⊆ u
rw [image2_singleton_left, image_subset_iff]